:: K\"onig's Theorem
:: by Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990 Association of Mizar Users


begin

definition
let IT be Function;
attr IT is Cardinal-yielding means :Def1: :: CARD_3:def 1
for x being set st x in dom IT holds
IT . x is Cardinal;
end;

:: deftheorem Def1 defines Cardinal-yielding CARD_3:def 1 :
for IT being Function holds
( IT is Cardinal-yielding iff for x being set st x in dom IT holds
IT . x is Cardinal );

registration
cluster empty Relation-like Function-like -> Cardinal-yielding set ;
coherence
for b1 being Function st b1 is empty holds
b1 is Cardinal-yielding
proof end;
end;

registration
cluster Relation-like Function-like Cardinal-yielding set ;
existence
ex b1 being Function st b1 is Cardinal-yielding
proof end;
end;

definition
mode Cardinal-Function is Cardinal-yielding Function;
end;

registration
let ff be Cardinal-Function;
let X be set ;
cluster ff | X -> Cardinal-yielding ;
coherence
ff | X is Cardinal-yielding
proof end;
end;

registration
let X be set ;
let K be Cardinal;
cluster X --> K -> Cardinal-yielding ;
coherence
X --> K is Cardinal-yielding
proof end;
end;

registration
let X be set ;
let K be Cardinal;
cluster X .--> K -> Cardinal-yielding ;
coherence
X .--> K is Cardinal-yielding
;
end;

theorem :: CARD_3:1
canceled;

theorem :: CARD_3:2
canceled;

theorem :: CARD_3:3
canceled;

scheme :: CARD_3:sch 1
CFLambda{ F1() -> set , F2( set ) -> Cardinal } :
ex ff being Cardinal-Function st
( dom ff = F1() & ( for x being set st x in F1() holds
ff . x = F2(x) ) )
proof end;

definition
let f be Function;
func Card f -> Cardinal-Function means :Def2: :: CARD_3:def 2
( dom it = dom f & ( for x being set st x in dom f holds
it . x = card (f . x) ) );
existence
ex b1 being Cardinal-Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = card (f . x) ) )
proof end;
uniqueness
for b1, b2 being Cardinal-Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = card (f . x) ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = card (f . x) ) holds
b1 = b2
proof end;
func disjoin f -> Function means :Def3: :: CARD_3:def 3
( dom it = dom f & ( for x being set st x in dom f holds
it . x = [:(f . x),{x}:] ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = [:(f . x),{x}:] ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = [:(f . x),{x}:] ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = [:(f . x),{x}:] ) holds
b1 = b2
proof end;
func Union f -> set equals :: CARD_3:def 4
union (rng f);
correctness
coherence
union (rng f) is set
;
;
defpred S1[ set ] means ex g being Function st
( $1 = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) );
func product f -> set means :Def5: :: CARD_3:def 5
for x being set holds
( x in it iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) ) & ( for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Card CARD_3:def 2 :
for f being Function
for b2 being Cardinal-Function holds
( b2 = Card f iff ( dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = card (f . x) ) ) );

:: deftheorem Def3 defines disjoin CARD_3:def 3 :
for f, b2 being Function holds
( b2 = disjoin f iff ( dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = [:(f . x),{x}:] ) ) );

:: deftheorem defines Union CARD_3:def 4 :
for f being Function holds Union f = union (rng f);

:: deftheorem Def5 defines product CARD_3:def 5 :
for f being Function
for b2 being set holds
( b2 = product f iff for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) );

theorem :: CARD_3:4
canceled;

theorem :: CARD_3:5
canceled;

theorem :: CARD_3:6
canceled;

theorem :: CARD_3:7
canceled;

theorem Th8: :: CARD_3:8
for ff being Cardinal-Function holds Card ff = ff
proof end;

theorem :: CARD_3:9
canceled;

theorem :: CARD_3:10
for X, Y being set holds Card (X --> Y) = X --> (card Y)
proof end;

theorem :: CARD_3:11
disjoin {} = {}
proof end;

theorem Th12: :: CARD_3:12
for x, X being set holds disjoin (x .--> X) = x .--> [:X,{x}:]
proof end;

theorem :: CARD_3:13
for x, y being set
for f being Function st x in dom f & y in dom f & x <> y holds
(disjoin f) . x misses (disjoin f) . y
proof end;

theorem :: CARD_3:14
canceled;

theorem Th15: :: CARD_3:15
for X, Y being set holds Union (X --> Y) c= Y
proof end;

theorem Th16: :: CARD_3:16
for X, Y being set st X <> {} holds
Union (X --> Y) = Y
proof end;

theorem :: CARD_3:17
for x, Y being set holds Union (x .--> Y) = Y by Th16;

theorem Th18: :: CARD_3:18
for g, f being Function holds
( g in product f iff ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) )
proof end;

theorem Th19: :: CARD_3:19
product {} = {{}}
proof end;

theorem Th20: :: CARD_3:20
for X, Y being set holds Funcs (X,Y) = product (X --> Y)
proof end;

defpred S1[ set ] means $1 is Function;

definition
let x, X be set ;
defpred S2[ set , set ] means ex g being Function st
( $1 = g & $2 = g . x );
func pi (X,x) -> set means :Def6: :: CARD_3:def 6
for y being set holds
( y in it iff ex f being Function st
( f in X & y = f . x ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ex f being Function st
( f in X & y = f . x ) )
proof end;
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ex f being Function st
( f in X & y = f . x ) ) ) & ( for y being set holds
( y in b2 iff ex f being Function st
( f in X & y = f . x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines pi CARD_3:def 6 :
for x, X, b3 being set holds
( b3 = pi (X,x) iff for y being set holds
( y in b3 iff ex f being Function st
( f in X & y = f . x ) ) );

theorem :: CARD_3:21
canceled;

theorem :: CARD_3:22
for x being set
for f being Function st x in dom f & product f <> {} holds
pi ((product f),x) = f . x
proof end;

theorem :: CARD_3:23
canceled;

theorem :: CARD_3:24
for x being set holds pi ({},x) = {}
proof end;

theorem :: CARD_3:25
for x being set
for g being Function holds pi ({g},x) = {(g . x)}
proof end;

theorem :: CARD_3:26
for x being set
for f, g being Function holds pi ({f,g},x) = {(f . x),(g . x)}
proof end;

theorem Th27: :: CARD_3:27
for X, Y, x being set holds pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))
proof end;

theorem :: CARD_3:28
for X, Y, x being set holds pi ((X /\ Y),x) c= (pi (X,x)) /\ (pi (Y,x))
proof end;

theorem Th29: :: CARD_3:29
for X, x, Y being set holds (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x)
proof end;

theorem :: CARD_3:30
for X, x, Y being set holds (pi (X,x)) \+\ (pi (Y,x)) c= pi ((X \+\ Y),x)
proof end;

theorem Th31: :: CARD_3:31
for X, x being set holds card (pi (X,x)) c= card X
proof end;

theorem Th32: :: CARD_3:32
for x being set
for f being Function st x in Union (disjoin f) holds
ex y, z being set st x = [y,z]
proof end;

theorem Th33: :: CARD_3:33
for x being set
for f being Function holds
( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
proof end;

theorem Th34: :: CARD_3:34
for f, g being Function st f c= g holds
disjoin f c= disjoin g
proof end;

theorem Th35: :: CARD_3:35
for f, g being Function st f c= g holds
Union f c= Union g
proof end;

theorem Th36: :: CARD_3:36
for Y, X being set holds Union (disjoin (Y --> X)) = [:X,Y:]
proof end;

theorem Th37: :: CARD_3:37
for f being Function holds
( product f = {} iff {} in rng f )
proof end;

theorem Th38: :: CARD_3:38
for f, g being Function st dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) holds
product f c= product g
proof end;

theorem :: CARD_3:39
for F being Cardinal-Function
for x being set st x in dom F holds
card (F . x) = F . x
proof end;

theorem Th40: :: CARD_3:40
for F being Cardinal-Function
for x being set st x in dom F holds
card ((disjoin F) . x) = F . x
proof end;

definition
let F be Cardinal-Function;
func Sum F -> Cardinal equals :: CARD_3:def 7
card (Union (disjoin F));
correctness
coherence
card (Union (disjoin F)) is Cardinal
;
;
func Product F -> Cardinal equals :: CARD_3:def 8
card (product F);
correctness
coherence
card (product F) is Cardinal
;
;
end;

:: deftheorem defines Sum CARD_3:def 7 :
for F being Cardinal-Function holds Sum F = card (Union (disjoin F));

:: deftheorem defines Product CARD_3:def 8 :
for F being Cardinal-Function holds Product F = card (product F);

theorem :: CARD_3:41
canceled;

theorem :: CARD_3:42
canceled;

theorem Th43: :: CARD_3:43
for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) holds
Sum F c= Sum G
proof end;

theorem :: CARD_3:44
for F being Cardinal-Function holds
( {} in rng F iff Product F = 0 )
proof end;

theorem :: CARD_3:45
for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) holds
Product F c= Product G by Th38, CARD_1:27;

theorem :: CARD_3:46
for F, G being Cardinal-Function st F c= G holds
Sum F c= Sum G
proof end;

theorem :: CARD_3:47
for F, G being Cardinal-Function st F c= G & not 0 in rng G holds
Product F c= Product G
proof end;

theorem :: CARD_3:48
for K being Cardinal holds Sum ({} --> K) = 0
proof end;

theorem :: CARD_3:49
for K being Cardinal holds Product ({} --> K) = 1 by Th19, CARD_1:50;

theorem :: CARD_3:50
for K being Cardinal
for x being set holds Sum (x .--> K) = K
proof end;

theorem :: CARD_3:51
for K being Cardinal
for x being set holds Product (x .--> K) = K
proof end;

theorem :: CARD_3:52
for M, N being Cardinal holds Sum (M --> N) = M *` N
proof end;

theorem :: CARD_3:53
for N, M being Cardinal holds Product (N --> M) = exp (M,N)
proof end;

theorem Th54: :: CARD_3:54
for f being Function holds card (Union f) c= Sum (Card f)
proof end;

theorem :: CARD_3:55
for F being Cardinal-Function holds card (Union F) c= Sum F
proof end;

theorem :: CARD_3:56
for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x in G . x ) holds
Sum F in Product G
proof end;

scheme :: CARD_3:sch 2
FinRegularity{ F1() -> finite set , P1[ set , set ] } :
ex x being set st
( x in F1() & ( for y being set st y in F1() & y <> x holds
not P1[y,x] ) )
provided
A1: F1() <> {} and
A2: for x, y being set st P1[x,y] & P1[y,x] holds
x = y and
A3: for x, y, z being set st P1[x,y] & P1[y,z] holds
P1[x,z]
proof end;

scheme :: CARD_3:sch 3
MaxFinSetElem{ F1() -> finite set , P1[ set , set ] } :
ex x being set st
( x in F1() & ( for y being set st y in F1() holds
P1[x,y] ) )
provided
A1: F1() <> {} and
A2: for x, y being set holds
( P1[x,y] or P1[y,x] ) and
A3: for x, y, z being set st P1[x,y] & P1[y,z] holds
P1[x,z]
proof end;

scheme :: CARD_3:sch 4
FuncSeparation{ F1() -> set , F2( set ) -> set , P1[ set , set ] } :
ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
for y being set holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) ) ) )
proof end;

Lm1: for n being Element of NAT st Rank n is finite holds
Rank (n + 1) is finite
proof end;

theorem :: CARD_3:57
for n being Element of NAT holds Rank n is finite
proof end;

Lm2: for x being set
for R being Relation st x in field R holds
ex y being set st
( [x,y] in R or [y,x] in R )
proof end;

theorem Th58: :: CARD_3:58
for X being set st X is finite holds
card X in card omega
proof end;

theorem Th59: :: CARD_3:59
for A, B being Ordinal st card A in card B holds
A in B
proof end;

theorem Th60: :: CARD_3:60
for A being Ordinal
for M being Cardinal st card A in M holds
A in M
proof end;

theorem Th61: :: CARD_3:61
for X being set st X is c=-linear holds
ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
proof end;

theorem :: CARD_3:62
for M being Cardinal
for X being set st ( for Z being set st Z in X holds
card Z in M ) & X is c=-linear holds
card (union X) c= M
proof end;

begin

registration
let f be Function;
cluster product f -> functional ;
coherence
product f is functional
proof end;
end;

registration
let A be set ;
let B be with_non-empty_elements set ;
cluster Function-like quasi_total -> non-empty Element of bool [:A,B:];
coherence
for b1 being Function of A,B holds b1 is non-empty
proof end;
end;

registration
let f be non-empty Function;
cluster product f -> non empty ;
coherence
not product f is empty
proof end;
end;

theorem :: CARD_3:63
for a, b, c, d being set st a <> b holds
product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))}
proof end;

theorem :: CARD_3:64
for x being set
for f being Function st x in product f holds
x is Function ;

begin

definition
let f be Function;
func sproduct f -> set means :Def9: :: CARD_3:def 9
for x being set holds
( x in it iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) ) & ( for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines sproduct CARD_3:def 9 :
for f being Function
for b2 being set holds
( b2 = sproduct f iff for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) );

registration
let f be Function;
cluster sproduct f -> non empty functional ;
coherence
( sproduct f is functional & not sproduct f is empty )
proof end;
end;

theorem Th65: :: CARD_3:65
for g, f being Function st g in sproduct f holds
( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) )
proof end;

theorem Th66: :: CARD_3:66
for f being Function holds {} in sproduct f
proof end;

registration
let f be Function;
cluster empty Relation-like Function-like Element of sproduct f;
existence
ex b1 being Element of sproduct f st b1 is empty
proof end;
end;

theorem Th67: :: CARD_3:67
for f being Function holds product f c= sproduct f
proof end;

theorem Th68: :: CARD_3:68
for x being set
for f being Function st x in sproduct f holds
x is PartFunc of (dom f),(union (rng f))
proof end;

theorem Th69: :: CARD_3:69
for g, f, h being Function st g in product f & h in sproduct f holds
g +* h in product f
proof end;

theorem :: CARD_3:70
for f, g being Function st product f <> {} holds
( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) )
proof end;

theorem Th71: :: CARD_3:71
for f being Function holds sproduct f c= PFuncs ((dom f),(union (rng f)))
proof end;

theorem Th72: :: CARD_3:72
for f, g being Function st f c= g holds
sproduct f c= sproduct g
proof end;

theorem Th73: :: CARD_3:73
sproduct {} = {{}}
proof end;

theorem :: CARD_3:74
for A, B being set holds PFuncs (A,B) = sproduct (A --> B)
proof end;

theorem :: CARD_3:75
for A, B being non empty set
for f being Function of A,B holds sproduct f = sproduct (f | { x where x is Element of A : f . x <> {} } )
proof end;

theorem Th76: :: CARD_3:76
for x, y being set
for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f
proof end;

theorem :: CARD_3:77
for f being Function holds
( sproduct f = {{}} iff for x being set st x in dom f holds
f . x = {} )
proof end;

theorem Th78: :: CARD_3:78
for f being Function
for A being set st A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) holds
union A in sproduct f
proof end;

theorem :: CARD_3:79
for g, h, f being Function st g tolerates h & g in sproduct f & h in sproduct f holds
g \/ h in sproduct f
proof end;

theorem Th80: :: CARD_3:80
for x being set
for h, f being Function st x c= h & h in sproduct f holds
x in sproduct f
proof end;

theorem Th81: :: CARD_3:81
for g, f being Function
for A being set st g in sproduct f holds
g | A in sproduct f by Th80, RELAT_1:88;

theorem Th82: :: CARD_3:82
for g, f being Function
for A being set st g in sproduct f holds
g | A in sproduct (f | A)
proof end;

theorem :: CARD_3:83
for h, f, g being Function st h in sproduct (f +* g) holds
ex f9, g9 being Function st
( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 )
proof end;

theorem Th84: :: CARD_3:84
for g, f, f9, g9 being Function st dom g misses (dom f9) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
proof end;

theorem :: CARD_3:85
for g, f, f9, g9 being Function st dom f9 misses (dom g) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
proof end;

theorem Th86: :: CARD_3:86
for g, f, h being Function st g in sproduct f & h in sproduct f holds
g +* h in sproduct f
proof end;

theorem :: CARD_3:87
for f being Function
for x1, x2, y1, y2 being set st x1 in dom f & y1 in f . x1 & x2 in dom f & y2 in f . x2 holds
(x1,x2) --> (y1,y2) in sproduct f
proof end;

begin

definition
let IT be set ;
attr IT is with_common_domain means :Def10: :: CARD_3:def 10
for f, g being Function st f in IT & g in IT holds
dom f = dom g;
end;

:: deftheorem Def10 defines with_common_domain CARD_3:def 10 :
for IT being set holds
( IT is with_common_domain iff for f, g being Function st f in IT & g in IT holds
dom f = dom g );

registration
cluster non empty functional with_common_domain set ;
existence
ex b1 being set st
( b1 is with_common_domain & b1 is functional & not b1 is empty )
proof end;
end;

theorem :: CARD_3:88
{{}} is functional with_common_domain set
proof end;

definition
let X be functional with_common_domain set ;
canceled;
func DOM X -> set means :Def12: :: CARD_3:def 12
for x being Function st x in X holds
it = dom x if X <> {}
otherwise it = {} ;
existence
( ( X <> {} implies ex b1 being set st
for x being Function st x in X holds
b1 = dom x ) & ( not X <> {} implies ex b1 being set st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( X <> {} & ( for x being Function st x in X holds
b1 = dom x ) & ( for x being Function st x in X holds
b2 = dom x ) implies b1 = b2 ) & ( not X <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being set holds verum
;
end;

:: deftheorem CARD_3:def 11 :
canceled;

:: deftheorem Def12 defines DOM CARD_3:def 12 :
for X being functional with_common_domain set
for b2 being set holds
( ( X <> {} implies ( b2 = DOM X iff for x being Function st x in X holds
b2 = dom x ) ) & ( not X <> {} implies ( b2 = DOM X iff b2 = {} ) ) );

theorem :: CARD_3:89
for X being functional with_common_domain set st X = {{}} holds
DOM X = {}
proof end;

begin

definition
let S be functional set ;
func product" S -> Function means :Def13: :: CARD_3:def 13
( ( for x being set holds
( x in dom it iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom it holds
it . i = pi (S,i) ) ) if not S is empty
otherwise it = {} ;
existence
( ( not S is empty implies ex b1 being Function st
( ( for x being set holds
( x in dom b1 iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) ) ) & ( S is empty implies ex b1 being Function st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being Function holds
( ( not S is empty & ( for x being set holds
( x in dom b1 iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) & ( for x being set holds
( x in dom b2 iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom b2 holds
b2 . i = pi (S,i) ) implies b1 = b2 ) & ( S is empty & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being Function holds verum
;
end;

:: deftheorem Def13 defines product" CARD_3:def 13 :
for S being functional set
for b2 being Function holds
( ( not S is empty implies ( b2 = product" S iff ( ( for x being set holds
( x in dom b2 iff for f being Function st f in S holds
x in dom f ) ) & ( for i being set st i in dom b2 holds
b2 . i = pi (S,i) ) ) ) ) & ( S is empty implies ( b2 = product" S iff b2 = {} ) ) );

theorem Th89: :: CARD_3:90
for S being non empty functional set holds dom (product" S) = meet { (dom f) where f is Element of S : verum }
proof end;

theorem Th90: :: CARD_3:91
for S being non empty functional set
for i being set st i in dom (product" S) holds
(product" S) . i = { (f . i) where f is Element of S : verum }
proof end;

definition
let S be set ;
attr S is product-like means :Def14: :: CARD_3:def 14
ex f being Function st S = product f;
end;

:: deftheorem Def14 defines product-like CARD_3:def 14 :
for S being set holds
( S is product-like iff ex f being Function st S = product f );

registration
let f be Function;
cluster product f -> product-like ;
coherence
product f is product-like
by Def14;
end;

registration
cluster product-like -> functional with_common_domain set ;
coherence
for b1 being set st b1 is product-like holds
( b1 is functional & b1 is with_common_domain )
proof end;
end;

registration
cluster non empty product-like set ;
existence
ex b1 being set st
( b1 is product-like & not b1 is empty )
proof end;
end;

theorem Th92: :: CARD_3:92
for S being functional with_common_domain set holds dom (product" S) = DOM S
proof end;

theorem :: CARD_3:93
for S being functional set
for i being set st i in dom (product" S) holds
(product" S) . i = pi (S,i)
proof end;

theorem Th94: :: CARD_3:94
for S being functional with_common_domain set holds S c= product (product" S)
proof end;

theorem :: CARD_3:95
for S being non empty product-like set holds S = product (product" S)
proof end;

theorem :: CARD_3:96
for f being Function
for s, t being Element of product f
for A being set holds s +* (t | A) is Element of product f
proof end;

theorem :: CARD_3:97
for f being non-empty Function
for p being Element of sproduct f ex s being Element of product f st p c= s
proof end;

theorem Th98: :: CARD_3:98
for g, f being Function
for A being set st g in product f holds
g | A in sproduct f
proof end;

definition
let f be non-empty Function;
let g be Element of product f;
let X be set ;
:: original: |
redefine func g | X -> Element of sproduct f;
coherence
g | X is Element of sproduct f
by Th98;
end;

theorem :: CARD_3:99
for f being non-empty Function
for s, ss being Element of product f
for A being set holds (ss +* (s | A)) | A = s | A
proof end;

theorem :: CARD_3:100
for M, x, g being Function st x in product M holds
x * g in product (M * g)
proof end;

theorem :: CARD_3:101
for X being set holds
( X is finite iff card X in omega ) by Th58, CARD_1:84;

theorem Th102: :: CARD_3:102
for A being Ordinal holds
( not A is finite iff omega c= A )
proof end;

theorem Th103: :: CARD_3:103
for N, M being Cardinal st N is finite & not M is finite holds
( N in M & N c= M )
proof end;

theorem :: CARD_3:104
for X being set holds
( not X is finite iff ex Y being set st
( Y c= X & card Y = omega ) )
proof end;

theorem Th105: :: CARD_3:105
for X, Y being set holds
( card X = card Y iff nextcard X = nextcard Y )
proof end;

theorem :: CARD_3:106
for N, M being Cardinal st nextcard N = nextcard M holds
M = N
proof end;

theorem Th107: :: CARD_3:107
for N, M being Cardinal holds
( N in M iff nextcard N c= M )
proof end;

theorem :: CARD_3:108
for N, M being Cardinal holds
( N in nextcard M iff N c= M )
proof end;

Lm3: 1 = card 1
by CARD_1:def 5;

Lm4: 2 = card 2
by CARD_1:def 5;

theorem :: CARD_3:109
for M being Cardinal holds
( 0 in M iff 1 c= M )
proof end;

theorem :: CARD_3:110
for M being Cardinal holds
( 1 in M iff 2 c= M )
proof end;

theorem Th111: :: CARD_3:111
for M, N being Cardinal st M is finite & ( N c= M or N in M ) holds
N is finite
proof end;

theorem Th112: :: CARD_3:112
for A being Ordinal holds
( A is limit_ordinal iff for B being Ordinal
for n being Nat st B in A holds
B +^ n in A )
proof end;

theorem Th113: :: CARD_3:113
for A being Ordinal
for n being Nat holds
( A +^ (succ n) = (succ A) +^ n & A +^ (n + 1) = (succ A) +^ n )
proof end;

theorem Th114: :: CARD_3:114
for A being Ordinal ex n being Nat st A *^ (succ 1) = A +^ n
proof end;

theorem Th115: :: CARD_3:115
for A being Ordinal st A is limit_ordinal holds
A *^ (succ 1) = A
proof end;

Lm5: omega is limit_ordinal
by ORDINAL1:def 12;

theorem Th116: :: CARD_3:116
for A being Ordinal st omega c= A holds
1 +^ A = A
proof end;

registration
cluster infinite cardinal -> limit_ordinal set ;
coherence
for b1 being Cardinal st not b1 is finite holds
b1 is limit_ordinal
proof end;
end;

theorem Th117: :: CARD_3:117
for M being Cardinal st not M is finite holds
M +` M = M
proof end;

theorem Th118: :: CARD_3:118
for M, N being Cardinal st not M is finite & ( N c= M or N in M ) holds
( M +` N = M & N +` M = M )
proof end;

theorem :: CARD_3:119
for X, Y being set st not X is finite & ( X,Y are_equipotent or Y,X are_equipotent ) holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
proof end;

theorem :: CARD_3:120
for X, Y being set st not X is finite & Y is finite holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
proof end;

theorem :: CARD_3:121
for X, Y being set st not X is finite & ( card Y in card X or card Y c= card X ) holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
proof end;

theorem :: CARD_3:122
for M, N being finite Cardinal holds M +` N is finite
proof end;

theorem :: CARD_3:123
for M, N being Cardinal st not M is finite holds
( not M +` N is finite & not N +` M is finite )
proof end;

theorem :: CARD_3:124
for M, N being finite Cardinal holds M *` N is finite
proof end;

theorem Th125: :: CARD_3:125
for K, L, M, N being Cardinal st ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) holds
( K +` M c= L +` N & M +` K c= L +` N )
proof end;

theorem :: CARD_3:126
for M, N, K being Cardinal st ( M in N or M c= N ) holds
( K +` M c= K +` N & K +` M c= N +` K & M +` K c= K +` N & M +` K c= N +` K ) by Th125;

definition
let X be set ;
attr X is countable means :Def15: :: CARD_3:def 15
card X c= omega ;
attr X is denumerable means :: CARD_3:def 16
card X = omega ;
end;

:: deftheorem Def15 defines countable CARD_3:def 15 :
for X being set holds
( X is countable iff card X c= omega );

:: deftheorem defines denumerable CARD_3:def 16 :
for X being set holds
( X is denumerable iff card X = omega );

registration
cluster denumerable -> infinite countable set ;
coherence
for b1 being set st b1 is denumerable holds
( b1 is countable & not b1 is finite )
proof end;
cluster infinite countable -> denumerable set ;
coherence
for b1 being set st b1 is countable & not b1 is finite holds
b1 is denumerable
proof end;
end;

registration
cluster finite -> countable set ;
coherence
for b1 being set st b1 is finite holds
b1 is countable
proof end;
end;

registration
cluster NAT -> denumerable ;
coherence
omega is denumerable
proof end;
end;

registration
cluster denumerable set ;
existence
ex b1 being set st b1 is denumerable
proof end;
end;

theorem Th127: :: CARD_3:127
for X being set holds
( X is countable iff ex f being Function st
( dom f = NAT & X c= rng f ) )
proof end;

registration
let X be countable set ;
cluster -> countable Element of bool X;
coherence
for b1 being Subset of X holds b1 is countable
proof end;
end;

Lm6: for Y, X being set st Y c= X & X is countable holds
Y is countable
;

theorem Th128: :: CARD_3:128
for X, Y being set st X is countable & Y is countable holds
X \/ Y is countable
proof end;

theorem :: CARD_3:129
for X, Y being set st X is countable holds
X /\ Y is countable by Lm6, XBOOLE_1:17;

theorem :: CARD_3:130
for X, Y being set st X is countable holds
X \ Y is countable ;

theorem :: CARD_3:131
for X, Y being set st X is countable & Y is countable holds
X \+\ Y is countable
proof end;

theorem Th132: :: CARD_3:132
for M, N being Cardinal
for f being Function st card (dom f) c= M & ( for x being set st x in dom f holds
card (f . x) c= N ) holds
card (Union f) c= M *` N
proof end;

theorem :: CARD_3:133
for M, N being Cardinal
for X being set st card X c= M & ( for Y being set st Y in X holds
card Y c= N ) holds
card (union X) c= M *` N
proof end;

theorem Th134: :: CARD_3:134
for f being Function st dom f is finite & ( for x being set st x in dom f holds
f . x is finite ) holds
Union f is finite
proof end;

theorem :: CARD_3:135
for n being Nat holds
( omega *` (card n) c= omega & (card n) *` omega c= omega )
proof end;

theorem Th136: :: CARD_3:136
for K, L, M, N being Cardinal st ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) holds
( K *` M c= L *` N & M *` K c= L *` N )
proof end;

theorem :: CARD_3:137
for M, N, K being Cardinal st ( M in N or M c= N ) holds
( K *` M c= K *` N & K *` M c= N *` K & M *` K c= K *` N & M *` K c= N *` K ) by Th136;

theorem Th138: :: CARD_3:138
for K, L, M, N being Cardinal holds
( ( not ( K in L & M in N ) & not ( K c= L & M in N ) & not ( K in L & M c= N ) & not ( K c= L & M c= N ) ) or K = 0 or exp (K,M) c= exp (L,N) )
proof end;

theorem :: CARD_3:139
for M, N, K being Cardinal holds
( ( not M in N & not M c= N ) or K = 0 or ( exp (K,M) c= exp (K,N) & exp (M,K) c= exp (N,K) ) )
proof end;

theorem Th140: :: CARD_3:140
for M, N being Cardinal holds
( M c= M +` N & N c= M +` N )
proof end;

theorem :: CARD_3:141
for N, M being Cardinal st N <> 0 holds
( M c= M *` N & M c= N *` M )
proof end;

theorem Th142: :: CARD_3:142
for K, L, M, N being Cardinal st K in L & M in N holds
( K +` M in L +` N & M +` K in L +` N )
proof end;

theorem :: CARD_3:143
for K, M, N being Cardinal st K +` M in K +` N holds
M in N
proof end;

theorem :: CARD_3:144
for X, Y being set st (card X) +` (card Y) = card X & card Y in card X holds
card (X \ Y) = card X
proof end;

theorem :: CARD_3:145
for K, M, N being Cardinal st K *` M in K *` N holds
M in N
proof end;

registration
let A be finite set ;
let B be set ;
let f be Function of A,(Fin B);
cluster Union f -> finite ;
coherence
Union f is finite
proof end;
end;

theorem :: CARD_3:146
for A being non empty countable set ex f being Function of NAT,A st rng f = A
proof end;

theorem :: CARD_3:147
for f, g being non-empty Function
for x being Element of product f
for y being Element of product g holds x +* y in product (f +* g)
proof end;

theorem :: CARD_3:148
for f, g being non-empty Function
for x being Element of product (f +* g) holds x | (dom g) in product g
proof end;

theorem :: CARD_3:149
for f, g being non-empty Function st f tolerates g holds
for x being Element of product (f +* g) holds x | (dom f) in product f
proof end;

theorem Th150: :: CARD_3:150
for S being functional with_common_domain set
for f being Function st f in S holds
dom f = dom (product" S)
proof end;

theorem Th151: :: CARD_3:151
for S being functional set
for f being Function
for i being set st f in S & i in dom (product" S) holds
f . i in (product" S) . i
proof end;

theorem :: CARD_3:152
for S being functional with_common_domain set
for f being Function
for i being set st f in S & i in dom f holds
f . i in (product" S) . i
proof end;

registration
let X be with_common_domain set ;
cluster -> with_common_domain Element of bool X;
coherence
for b1 being Subset of X holds b1 is with_common_domain
proof end;
end;

definition
let f be Function;
let x be set ;
func proj (f,x) -> Function means :Def17: :: CARD_3:def 17
( dom it = product f & ( for y being Function st y in dom it holds
it . y = y . x ) );
existence
ex b1 being Function st
( dom b1 = product f & ( for y being Function st y in dom b1 holds
b1 . y = y . x ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = product f & ( for y being Function st y in dom b1 holds
b1 . y = y . x ) & dom b2 = product f & ( for y being Function st y in dom b2 holds
b2 . y = y . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines proj CARD_3:def 17 :
for f being Function
for x being set
for b3 being Function holds
( b3 = proj (f,x) iff ( dom b3 = product f & ( for y being Function st y in dom b3 holds
b3 . y = y . x ) ) );

registration
let f be Function;
let x be set ;
cluster proj (f,x) -> product f -defined ;
coherence
proj (f,x) is product f -defined
proof end;
end;

registration
let f be Function;
let x be set ;
cluster proj (f,x) -> total ;
coherence
proj (f,x) is total
proof end;
end;

registration
let f be non-empty Function;
cluster -> f -compatible Element of product f;
coherence
for b1 being Element of product f holds b1 is f -compatible
proof end;
end;

registration
let I be set ;
let f be non-empty I -defined Function;
cluster -> I -defined Element of product f;
coherence
for b1 being Element of product f holds b1 is I -defined
proof end;
end;

registration
let f be Function;
cluster -> f -compatible Element of sproduct f;
coherence
for b1 being Element of sproduct f holds b1 is f -compatible
proof end;
end;

registration
let I be set ;
let f be I -defined Function;
cluster -> I -defined Element of sproduct f;
coherence
for b1 being Element of sproduct f holds b1 is I -defined
proof end;
end;

registration
let I be set ;
let f be non-empty I -defined total Function;
cluster -> total Element of product f;
coherence
for b1 being Element of product f holds b1 is total
proof end;
end;

theorem Th153: :: CARD_3:153
for I being set
for f being non-empty b1 -defined Function
for p being b1 -defined b2 -compatible Function holds p in sproduct f
proof end;

theorem :: CARD_3:154
for I being set
for f being non-empty b1 -defined Function
for p being b1 -defined b2 -compatible Function ex s being Element of product f st p c= s
proof end;

registration
let X be infinite set ;
let a be set ;
cluster X --> a -> infinite ;
coherence
not X --> a is finite
;
end;

registration
cluster Relation-like Function-like infinite set ;
existence
not for b1 being Function holds b1 is finite
proof end;
end;

registration
let R be infinite Relation;
cluster field R -> infinite ;
coherence
not field R is finite
by ORDERS_1:196;
end;

registration
let X be infinite set ;
cluster RelIncl X -> infinite ;
coherence
not RelIncl X is finite
by CARD_1:105;
end;

theorem :: CARD_3:155
for R, S being Relation st R,S are_isomorphic & R is finite holds
S is finite
proof end;

theorem :: CARD_3:156
product" {{}} = {}
proof end;