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


definition
let IT be Function;
attr IT is Cardinal-yielding means :Def1: :: CARD_3:def 1
 for x being object 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 object st x in dom IT holds
IT . x is Cardinal );

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

registration
cluster Relation-like Function-like Cardinal-yielding for 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 object ;
let K be Cardinal;
cluster X .--> K -> Cardinal-yielding ;
coherence
X .--> K is Cardinal-yielding ;
end;

scheme :: CARD_3:sch 1
CFLambda{ F1() -> set , F2( object ) -> 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 object 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 object 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 object st x in dom f holds
b1 . x = card (f . x) ) & dom b2 = dom f & ( for x being object 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 object st x in dom f holds
it . x = [:(f . x),{x}:] ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being object 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 object st x in dom f holds
b1 . x = [:(f . x),{x}:] ) & dom b2 = dom f & ( for x being object 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[ object ] means ex g being Function st
( $1 = g & dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) );
func product f -> set means :Def5: :: CARD_3:def 5
 for x being object holds
( x in it iff ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) ) ) & ( for x being object holds
( x in b2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being object 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 object 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 object 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 object holds
( x in b2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) ) );

theorem Th1: :: CARD_3:1
for ff being Cardinal-Function holds Card ff = ff
proof end;

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

theorem :: CARD_3:3
disjoin {} = {} by Def3, RELAT_1:38;

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

theorem :: CARD_3:5
for x, y being object
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 Th6: :: CARD_3:6
for X, Y being set holds Union (X --> Y) c= Y
proof end;

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

theorem :: CARD_3:8
for x being object
for Y being set holds Union (x .--> Y) = Y by Th7;

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

theorem Th10: :: CARD_3:10
product {} = {{}}
proof end;

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

defpred S1[ object ] means $1 is Function;

definition
let x be object ;
let X be set ;
defpred S2[ object , object ] 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 object 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 object 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 object holds
( y in b1 iff ex f being Function st
( f in X & y = f . x ) ) ) & ( for y being object 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 being object
for X, b3 being set holds
( b3 = pi (X,x) iff for y being object holds
( y in b3 iff ex f being Function st
( f in X & y = f . x ) ) );

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

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

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

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

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

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

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

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

theorem Th20: :: CARD_3:20
for x being object
for X being set holds card (pi (X,x)) c= card X
proof end;

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

theorem Th22: :: CARD_3:22
for x being object
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 Th23: :: CARD_3:23
for f, g being Function st f c= g holds
disjoin f c= disjoin g
proof end;

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

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

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

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

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

theorem Th29: :: CARD_3:29
for F being Cardinal-Function
for x being object 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:30
for F, G being Cardinal-Function st dom F = dom G & ( for x being object st x in dom F holds
F . x c= G . x ) holds
Sum F c= Sum G
proof end;

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

theorem :: CARD_3:32
for F, G being Cardinal-Function st dom F = dom G & ( for x being object st x in dom F holds
F . x c= G . x ) holds
Product F c= Product G by Th27, CARD_1:11;

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

theorem :: CARD_3:34
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:35
for K being Cardinal holds Sum ({} --> K) = 0
proof end;

theorem :: CARD_3:36
for K being Cardinal holds Product ({} --> K) = 1 by Th10, CARD_1:30;

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

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

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

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

:: WP: Koenig Theorem
theorem :: CARD_3:41
for F, G being Cardinal-Function st dom F = dom G & ( for x being object st x in dom F holds
F . x in G . x ) holds
Sum F in Product G
proof end;

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

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

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

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

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

theorem Th45: :: CARD_3:45
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:46
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;

:: from AMI_1
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 for Element of bool [:A,B:];
coherence
for b1 being Function of A,B holds b1 is non-empty
proof end;
end;

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

:: from AMI_1, 2006.03.14, A.T.
theorem :: CARD_3:47
for a, b, c, d being set st a <> b holds
product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))}
proof end;

:: from AMI_1, 2006.03.14, A.T.
theorem :: CARD_3:48
for x being object
for f being Function st x in product f holds
x is Function ;

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

theorem Th50: :: CARD_3:50
for f being Function holds {} in sproduct f
proof end;

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

theorem Th51: :: CARD_3:51
for f being Function holds product f c= sproduct f
proof end;

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

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

theorem :: CARD_3:54
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 Th55: :: CARD_3:55
for f being Function holds sproduct f c= PFuncs ((dom f),(union (rng f)))
proof end;

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

theorem Th57: :: CARD_3:57
sproduct {} = {{}}
proof end;

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

theorem :: CARD_3:59
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 Th60: :: CARD_3:60
for x, y being object
for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f
proof end;

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

theorem Th62: :: CARD_3:62
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:63
for f, g, h being Function st g tolerates h & g in sproduct f & h in sproduct f holds
g \/ h in sproduct f
proof end;

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

theorem Th65: :: CARD_3:65
for f, g being Function
for A being set st g in sproduct f holds
g | A in sproduct f by Th64, RELAT_1:59;

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

theorem :: CARD_3:67
for f, g, h 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 Th68: :: CARD_3:68
for f, g, 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:69
for f, g, 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 Th70: :: CARD_3:70
for f, g, h being Function st g in sproduct f & h in sproduct f holds
g +* h in sproduct f
proof end;

theorem :: CARD_3:71
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;

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 for set ;
existence
ex b1 being set st
( b1 is with_common_domain & b1 is functional & not b1 is empty )
proof end;
end;

registration
let f be Function;
cluster {f} -> with_common_domain ;
coherence
{f} is with_common_domain
proof end;
end;

definition
let X be functional set ;
func DOM X -> set equals :: CARD_3:def 11
 meet { (dom f) where f is Element of X : verum } ;
coherence
meet { (dom f) where f is Element of X : verum } is set ;
end;

:: deftheorem defines DOM CARD_3:def 11 :
for X being functional set holds DOM X = meet { (dom f) where f is Element of X : verum } ;

Lm2: for X being functional with_common_domain set
for f being Function st f in X holds
dom f = DOM X
proof end;

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

registration
let X be empty set ;
cluster DOM X -> empty ;
coherence
DOM X is empty
proof end;
end;

definition
let S be functional set ;
func product" S -> Function means :Def12: :: CARD_3:def 12
( dom it = DOM S & ( for i being set st i in dom it holds
it . i = pi (S,i) ) );
existence
ex b1 being Function st
( dom b1 = DOM S & ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = DOM S & ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) & dom b2 = DOM S & ( for i being set st i in dom b2 holds
b2 . i = pi (S,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines product" CARD_3:def 12 :
for S being functional set
for b2 being Function holds
( b2 = product" S iff ( dom b2 = DOM S & ( for i being set st i in dom b2 holds
b2 . i = pi (S,i) ) ) );

theorem :: CARD_3:73
canceled;

::$CT
theorem Th73: :: CARD_3:74
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 :Def13: :: CARD_3:def 13
 ex f being Function st S = product f;
end;

:: deftheorem Def13 defines product-like CARD_3:def 13 :
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 ;
end;

registration
cluster product-like -> functional with_common_domain for 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 for set ;
existence
ex b1 being set st
( b1 is product-like & not b1 is empty )
proof end;
end;

theorem :: CARD_3:75
canceled;

theorem :: CARD_3:76
canceled;

::$CT 2
theorem Th74: :: CARD_3:77
for S being functional with_common_domain set holds S c= product (product" S)
proof end;

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

:: from AMI_1, 2008.04.11, A.T. (generalized)
theorem :: CARD_3:79
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:80
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 Th78: :: CARD_3:81
for f, g being Function
for A being set st g in product f holds
g | A in sproduct f
proof end;

:: needed, 2008.04.20, A.T.
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 Th78;
end;

theorem :: CARD_3:82
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;

:: from PRE_CIRC, 2008.06.02, A.T.
theorem :: CARD_3:83
for M, x, g being Function st x in product M holds
x * g in product (M * g)
proof end;

:: moved from CARD_4, 2008.10.08, A.T.
theorem :: CARD_3:84
for X being set holds
( X is finite iff card X in omega ) by Th42;

theorem Th82: :: CARD_3:85
for A being Ordinal holds
( A is infinite iff omega c= A )
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th90: :: CARD_3:93
for X being set holds
( X is countable iff ex f being Function st
( dom f = omega & X c= rng f ) ) by CARD_1:12, CARD_1:47;

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

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

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

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

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

:: from CIRCCOMB, 2009.01.26, A.T.
theorem :: CARD_3:97
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:98
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:99
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;

:: missing, 2009.09.06, A.T.
theorem Th97: :: CARD_3:100
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 Th98: :: CARD_3:101
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:102
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;

:: 2009.09.12, A.T.
registration
let X be with_common_domain set ;
cluster -> with_common_domain for Element of bool X;
coherence
for b1 being Subset of X holds b1 is with_common_domain by Def10;
end;

:: from PRALG_3, 2009.09.18, A.T.
definition
let f be Function;
let x be object ;
func proj (f,x) -> Function means :Def16: :: CARD_3:def 16
( 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 Def16 defines proj CARD_3:def 16 :
for f being Function
for x being object
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 object ;
cluster proj (f,x) -> product f -defined ;
coherence
proj (f,x) is product f -defined by Def16;
end;

registration
let f be Function;
let x be object ;
cluster proj (f,x) -> total ;
coherence
proj (f,x) is total by Def16;
end;

registration
let f be non-empty Function;
cluster -> f -compatible for 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 for Element of product f;
coherence
for b1 being Element of product f holds b1 is I -defined ;
end;

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

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

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

theorem Th100: :: CARD_3:103
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:104
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;

:: from AMISTD_2, 2010.01.10, A.T
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 for set ;
existence
ex b1 being Function st b1 is infinite
proof end;
end;

Lm4: for R being Relation st field R is finite holds
R is finite
proof end;

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

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

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

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

theorem Th104: :: CARD_3:107
for I being set
for f being V8() ManySortedSet of I
for s being b2 -compatible ManySortedSet of I holds s in product f
proof end;

registration
let I be set ;
let f be V8() ManySortedSet of I;
cluster -> total for Element of product f;
coherence
for b1 being Element of product f holds b1 is total ;
end;

definition
let I be set ;
let f be V8() ManySortedSet of I;
let M be f -compatible ManySortedSet of I;
func down M -> Element of product f equals :: CARD_3:def 17
M;
coherence
M is Element of product f by Th104;
end;

:: deftheorem defines down CARD_3:def 17 :
for I being set
for f being V8() ManySortedSet of I
for M being b2 -compatible ManySortedSet of I holds down M = M;

theorem :: CARD_3:108
for X being functional with_common_domain set
for f being Function st f in X holds
dom f = DOM X by Lm2;

theorem :: CARD_3:109
for x being object
for X being non empty functional set st ( for f being Function st f in X holds
x in dom f ) holds
x in DOM X
proof end;

scheme :: CARD_3:sch 3
FuncSepOrg{ F1() -> set , F2( object ) -> set , P1[ object , object ] } :
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;

notation
let X be set ;
antonym uncountable X for countable ;
end;

registration
cluster uncountable -> non empty for set ;
coherence
for b1 being set st b1 is uncountable holds
not b1 is empty ;
end;