CARD_1

set A = the Ordinal;
defpred S₁[ Ordinal] means c₁, the Ordinal are_equipotent ;
A1: ex A being Ordinal st S₁[A] ;
consider B being Ordinal such that
A2: ( S₁[B] & ( for C being Ordinal st S₁[C] holds
B c= C ) ) from ORDINAL1:sch 1(A1);
reconsider IT = B as set ;
take IT ; :: thesis:
take B ; :: according to CARD_1:def 1 :: thesis:
thus ( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) ) by A2, WELLORD2:15; :: thesis:

end;

definition

mode Cardinal is cardinal set ;

end;

registration

cluster cardinal -> ordinal for set ;

end;

theorem :: CARD_1:1

canceled;

theorem Th1: :: CARD_1:2

for M, N being Cardinal st M,N are_equipotent holds
M = N

let M, N be Cardinal; :: thesis:
A1: ex A being Ordinal st
( M = A & ( for C being Ordinal st C,A are_equipotent holds
A c= C ) ) by Def1;
ex B being Ordinal st
( N = B & ( for C being Ordinal st C,B are_equipotent holds
B c= C ) ) by Def1;
hence ( M,N are_equipotent implies M = N ) by A1; :: thesis:

end;

theorem :: CARD_1:3

for M, N being Cardinal holds
( M in N iff ( M c= N & M <> N ) ) by ORDINAL1:11, XBOOLE_0:def 8;

theorem :: CARD_1:4

for M, N being Cardinal holds
( M in N iff not N c= M ) by ORDINAL1:5, ORDINAL1:16;

definition

let X be set ;

func card X -> Cardinal means :Def2: :: CARD_1:def 2
X,it are_equipotent ;

defpred S₁[ Ordinal] means X,$1 are_equipotent ;
consider R being Relation such that
A1: R well_orders X by WELLORD2:17;
set Q = R |_2 X;
set A = order_type_of (R |_2 X);
R |_2 X is well-ordering by A1, WELLORD2:16;
then R |_2 X, RelIncl (order_type_of (R |_2 X)) are_isomorphic by WELLORD2:def 2;
then consider f being Function such that
A2: f is_isomorphism_of R |_2 X, RelIncl (order_type_of (R |_2 X)) by WELLORD1:def 8;
X, order_type_of (R |_2 X) are_equipotent

take f ; :: according to WELLORD2:def 4 :: thesis:
( dom f = field (R |_2 X) & rng f = field (RelIncl (order_type_of (R |_2 X))) ) by A2, WELLORD1:def 7;
hence ( f is one-to-one & dom f = X & rng f = order_type_of (R |_2 X) ) by A1, A2, WELLORD1:def 7, WELLORD2:16, WELLORD2:def 1; :: thesis:

end;

then A3: ex A being Ordinal st S₁[A] ;
consider A being Ordinal such that
A4: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A3);
A is cardinal

take A ; :: according to CARD_1:def 1 :: thesis:
thus A = A ; :: thesis:
let B be Ordinal; :: thesis:
assume B,A are_equipotent ; :: thesis:
hence A c= B by A4, WELLORD2:15; :: thesis:

end;

then reconsider M = A as Cardinal ;
take M ; :: thesis:
thus X,M are_equipotent by A4; :: thesis:

end;

uniqueness by Th1, WELLORD2:15;
projectivity ;

end;

:: deftheorem Def2 defines card CARD_1:def 2 :

registration

let C be Cardinal;

reduce card C to C;

reducibility by Def2;

end;

registration

cluster empty -> cardinal for set ;

let S be set ; :: thesis:
assume A1: S is empty ; :: thesis:
take {} ; :: according to CARD_1:def 1 :: thesis:
thus S = {} by A1; :: thesis:
let A be Ordinal; :: thesis:
assume A, {} are_equipotent ; :: thesis:
thus {} c= A ; :: thesis:

end;

registration

let X be empty set ;

cluster card X -> empty ;

end;

registration

let X be empty set ;

cluster card X -> zero ;

end;

registration

let X be non empty set ;

cluster card X -> non empty ;

assume card X is empty ; :: thesis:
then ex f being Function st
( f is one-to-one & dom f = X & rng f = {} ) by Def2, WELLORD2:def 4;
hence contradiction by RELAT_1:42; :: thesis:

end;

registration

let X be non empty set ;

cluster card X -> non zero ;

end;

theorem Th4: :: CARD_1:5

for X, Y being set holds
( X,Y are_equipotent iff card X = card Y )

let X, Y be set ; :: thesis:
A1: Y, card Y are_equipotent by Def2;
A2: X, card X are_equipotent by Def2;
hence ( X,Y are_equipotent implies card X = card Y ) by Def2, WELLORD2:15; :: thesis:
assume card X = card Y ; :: thesis:
hence X,Y are_equipotent by A2, A1, WELLORD2:15; :: thesis:

end;

theorem Th5: :: CARD_1:6

for R being Relation st R is well-ordering holds
field R, order_type_of R are_equipotent

let R be Relation; :: thesis:
assume R is well-ordering ; :: thesis:
then R, RelIncl (order_type_of R) are_isomorphic by WELLORD2:def 2;
then consider f being Function such that
A1: f is_isomorphism_of R, RelIncl (order_type_of R) by WELLORD1:def 8;
take f ; :: according to WELLORD2:def 4 :: thesis:
field (RelIncl (order_type_of R)) = order_type_of R by WELLORD2:def 1;
hence ( f is one-to-one & dom f = field R & rng f = order_type_of R ) by A1, WELLORD1:def 7; :: thesis:

end;

theorem Th6: :: CARD_1:7

for X being set
for M being Cardinal st X c= M holds
card X c= M

let X be set ; :: thesis:
let M be Cardinal; :: thesis:
defpred S₁[ Ordinal] means ( $1 c= M & X,$1 are_equipotent );
reconsider m = M as Ordinal ;
assume X c= M ; :: thesis:
then A1: ( order_type_of (RelIncl X) c= m & RelIncl X is well-ordering ) by WELLORD2:8, WELLORD2:14;
field (RelIncl X) = X by WELLORD2:def 1;
then A2: ex A being Ordinal st S₁[A] by A1, Th5;
consider A being Ordinal such that
A3: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A2);
A is cardinal

take A ; :: according to CARD_1:def 1 :: thesis:
thus A = A ; :: thesis:
let B be Ordinal; :: thesis:
assume A4: B,A are_equipotent ; :: thesis:
assume A5: not A c= B ; :: thesis:
then m c= B by A3, A4, WELLORD2:15;
hence contradiction by A3, A5; :: thesis:

end;

then reconsider A = A as Cardinal ;
card X = A by A3, Def2;
hence card X c= M by A3; :: thesis:

end;

theorem Th7: :: CARD_1:8

for A being Ordinal holds card A c= A

let A be Ordinal; :: thesis:
( ex B being Ordinal st
( card A = B & ( for C being Ordinal st C,B are_equipotent holds
B c= C ) ) & A, card A are_equipotent ) by Def1, Def2;
hence card A c= A ; :: thesis:

end;

theorem :: CARD_1:9

for X being set
for M being Cardinal st X in M holds
card X in M by Th7, ORDINAL1:12;

theorem Th9: :: CARD_1:10

for X, Y being set holds
( card X c= card Y iff ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) )

let X, Y be set ; :: thesis:
thus ( card X c= card Y implies ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) ) :: thesis:

consider f being Function such that
A1: f is one-to-one and
A2: ( dom f = X & rng f = card X ) by Def2, WELLORD2:def 4;
assume A3: card X c= card Y ; :: thesis:
consider g being Function such that
A4: g is one-to-one and
A5: ( dom g = Y & rng g = card Y ) by Def2, WELLORD2:def 4;
take h = (g ") * f; :: thesis:
thus h is one-to-one by A1, A4; :: thesis:
( rng g = dom (g ") & dom g = rng (g ") ) by A4, FUNCT_1:33;
hence ( dom h = X & rng h c= Y ) by A3, A2, A5, RELAT_1:26, RELAT_1:27; :: thesis:

end;

given f being Function such that A6: f is one-to-one and
A7: ( dom f = X & rng f c= Y ) ; :: thesis:
consider g being Function such that
A8: g is one-to-one and
A9: dom g = Y and
A10: rng g = card Y by Def2, WELLORD2:def 4;
A11: X, rng (g * f) are_equipotent

take g * f ; :: according to WELLORD2:def 4 :: thesis:
thus g * f is one-to-one by A6, A8; :: thesis:
thus dom (g * f) = X by A7, A9, RELAT_1:27; :: thesis:
thus rng (g * f) = rng (g * f) ; :: thesis:

end;

A12: rng (g * f), card (rng (g * f)) are_equipotent by Def2;
card (rng (g * f)) c= card Y by A10, Th6, RELAT_1:26;
hence card X c= card Y by A12, Def2, A11, WELLORD2:15; :: thesis:

end;

theorem Th10: :: CARD_1:11

for X, Y being set st X c= Y holds
card X c= card Y

let X, Y be set ; :: thesis:
assume A1: X c= Y ; :: thesis:
ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y )

take id X ; :: thesis:
thus ( id X is one-to-one & dom (id X) = X & rng (id X) c= Y ) by A1, RELAT_1:45; :: thesis:

end;

hence card X c= card Y by Th9; :: thesis:

end;

theorem Th11: :: CARD_1:12

for X, Y being set holds
( card X c= card Y iff ex f being Function st
( dom f = Y & X c= rng f ) )

let X, Y be set ; :: thesis:
thus ( card X c= card Y implies ex f being Function st
( dom f = Y & X c= rng f ) ) :: thesis:

assume card X c= card Y ; :: thesis:
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f c= Y by Th9;
defpred S₁[ object , object ] means ( ( $1 in rng f & $2 = (f ") . $1 ) or ( not $1 in rng f & $2 = 0 ) );
A4: for x being object st x in Y holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in Y ; :: thesis:
( not x in rng f implies ex y being object st S₁[x,y] ) ;
hence ex y being object st S₁[x,y] ; :: thesis:

end;

A5: for x, y, z being object st x in Y & S₁[x,y] & S₁[x,z] holds
y = z ;
consider g being Function such that
A6: ( dom g = Y & ( for y being object st y in Y holds
S₁[y,g . y] ) ) from FUNCT_1:sch 2(A5, A4);
take g ; :: thesis:
thus dom g = Y by A6; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in X ; :: thesis:
then A8: f . x in rng f by A2, FUNCT_1:def 3;
(f ") . (f . x) = x by A1, A2, A7, FUNCT_1:34;
then x = g . (f . x) by A3, A6, A8;
hence x in rng g by A3, A6, A8, FUNCT_1:def 3; :: thesis:

end;

given f being Function such that A9: dom f = Y and
A10: X c= rng f ; :: thesis:
deffunc H₁( object ) -> set = f " {$1};
consider g being Function such that
A11: ( dom g = X & ( for x being object st x in X holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();

per cases ;

suppose X <> {} ; :: thesis:

then reconsider M = rng g as non empty set by A11, RELAT_1:42;
for Z being set st Z in M holds
Z <> {}

let Z be set ; :: thesis:
assume Z in M ; :: thesis:
then consider x being object such that
A12: ( x in dom g & Z = g . x ) by FUNCT_1:def 3;
A13: x in {x} by TARSKI:def 1;
( Z = f " {x} & ex y being object st
( y in dom f & x = f . y ) ) by A10, A11, A12, FUNCT_1:def 3;
hence Z <> {} by A13, FUNCT_1:def 7; :: thesis:

end;

then consider F being Function such that
A14: dom F = M and
A15: for Z being set st Z in M holds
F . Z in Z by FUNCT_1:111;
A16: dom (F * g) = X by A11, A14, RELAT_1:27;
A17: F * g is one-to-one

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A18: x in dom (F * g) and
A19: y in dom (F * g) and
A20: (F * g) . x = (F * g) . y ; :: thesis:
A21: g . y = f " {y} by A11, A16, A19;
then f " {y} in M by A11, A16, A19, FUNCT_1:def 3;
then F . (f " {y}) in f " {y} by A15;
then A22: f . (F . (f " {y})) in {y} by FUNCT_1:def 7;
A23: g . x = f " {x} by A11, A16, A18;
then f " {x} in M by A11, A16, A18, FUNCT_1:def 3;
then F . (f " {x}) in f " {x} by A15;
then f . (F . (f " {x})) in {x} by FUNCT_1:def 7;
then A24: f . (F . (f " {x})) = x by TARSKI:def 1;
( (F * g) . x = F . (g . x) & (F * g) . y = F . (g . y) ) by A11, A16, A18, A19, FUNCT_1:13;
hence x = y by A20, A23, A21, A22, A24, TARSKI:def 1; :: thesis:

end;

rng (F * g) c= Y

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (F * g) ; :: thesis:
then consider y being object such that
A25: y in dom (F * g) and
A26: x = (F * g) . y by FUNCT_1:def 3;
A27: x = F . (g . y) by A11, A16, A25, A26, FUNCT_1:13;
A28: g . y = f " {y} by A11, A16, A25;
then f " {y} in M by A11, A16, A25, FUNCT_1:def 3;
then x in f " {y} by A15, A28, A27;
hence x in Y by A9, FUNCT_1:def 7; :: thesis:

end;

hence card X c= card Y by A16, A17, Th9; :: thesis:

end;

suppose X = {} ; :: thesis:

hence card X c= card Y ; :: thesis:

end;

theorem Th12: :: CARD_1:13

for X being set holds not X, bool X are_equipotent

let X be set ; :: thesis:
given f being Function such that f is one-to-one and
A1: ( dom f = X & rng f = bool X ) ; :: according to WELLORD2:def 4 :: thesis:
defpred S₁[ object ] means for Y being set st Y = f . $1 holds
not $1 in Y;
consider Z being set such that
A2: for a being object holds
( a in Z iff ( a in X & S₁[a] ) ) from XBOOLE_0:sch 1();
Z c= X by A2;
then consider a being object such that
A3: a in X and
A4: Z = f . a by A1, FUNCT_1:def 3;
ex Y being set st
( Y = f . a & a in Y ) by A2, A3, A4;
hence contradiction by A2, A4; :: thesis:

end;

theorem Th13: :: CARD_1:14

for X being set holds card X in card (bool X)

let X be set ; :: thesis:
deffunc H₁( object ) -> set = {$1};
consider f being Function such that
A1: ( dom f = X & ( for x being object st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
A2: rng f c= bool X

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def 3;
A5: {y} c= X by A1, A3, TARSKI:def 1;
f . y = {y} by A1, A3;
hence x in bool X by A4, A5; :: thesis:

end;

A6: card X <> card (bool X) by Th4, Th12;
f is one-to-one

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A7: ( x in dom f & y in dom f ) and
A8: f . x = f . y ; :: thesis:
( f . x = {x} & f . y = {y} ) by A1, A7;
hence x = y by A8, ZFMISC_1:3; :: thesis:

end;

then card X c= card (bool X) by A1, A2, Th9;
hence card X in card (bool X) by A6, ORDINAL1:11, XBOOLE_0:def 8; :: thesis:

end;

definition

let X be set ;

func nextcard X -> Cardinal means :Def3: :: CARD_1:def 3
( card X in it & ( for M being Cardinal st card X in M holds
it c= M ) );

defpred S₁[ Ordinal] means ex M being Cardinal st
( $1 = M & card X in M );
card X in card (bool X) by Th13;
then A1: ex A being Ordinal st S₁[A] ;
consider A being Ordinal such that
A2: S₁[A] and
A3: for B being Ordinal st S₁[B] holds
A c= B from ORDINAL1:sch 1(A1);
consider M being Cardinal such that
A4: A = M and
A5: card X in M by A2;
take M ; :: thesis:
thus card X in M by A5; :: thesis:
let N be Cardinal; :: thesis:
assume card X in N ; :: thesis:
hence M c= N by A3, A4; :: thesis:

end;

uniqueness ;

end;

:: deftheorem Def3 defines nextcard CARD_1:def 3 :

theorem :: CARD_1:15

for X being set holds {} in nextcard X

let X be set ; :: thesis:
( card {} c= card X & card X in nextcard X ) by Def3;
hence {} in nextcard X by ORDINAL1:12; :: thesis:

end;

theorem Th15: :: CARD_1:16

for X, Y being set st card X = card Y holds
nextcard X = nextcard Y

let X, Y be set ; :: thesis:
assume A1: card X = card Y ; :: thesis:
( card X in nextcard X & ( for N being Cardinal st card X in N holds
nextcard X c= N ) ) by Def3;
hence nextcard X = nextcard Y by A1, Def3; :: thesis:

end;

theorem Th16: :: CARD_1:17

for X, Y being set st X,Y are_equipotent holds
nextcard X = nextcard Y

let X, Y be set ; :: thesis:
assume X,Y are_equipotent ; :: thesis:
then card X = card Y by Th4;
hence nextcard X = nextcard Y by Th15; :: thesis:

end;

theorem Th17: :: CARD_1:18

for A being Ordinal holds A in nextcard A

let A be Ordinal; :: thesis:
assume not A in nextcard A ; :: thesis:
then A1: card (nextcard A) c= card A by Th10, ORDINAL1:16;
A2: nextcard (card A) = nextcard A by Def2, Th16;
A3: card (card A) in nextcard (card A) by Def3;
thus contradiction by A1, A2, A3, ORDINAL1:5; :: thesis:

end;

definition

let M be Cardinal;

attr M is limit_cardinal means :: CARD_1:def 4
for N being Cardinal holds not M = nextcard N;

end;

:: deftheorem defines limit_cardinal CARD_1:def 4 :

definition

let A be Ordinal;

func aleph A -> set means :Def5: :: CARD_1:def 5
ex S being Sequence st
( it = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) );

correctness

set B = card omega;
deffunc H₁( Ordinal, Sequence) -> Cardinal = card (sup $2);
deffunc H₂( Ordinal, set ) -> Cardinal = nextcard $2;
( ex x being object ex S being Sequence st
( x = last S & dom S = succ A & S . 0 = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H₂(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
S . C = H₁(C,S | C) ) ) & ( for x1, x2 being set st ex S being Sequence st
( x1 = last S & dom S = succ A & S . 0 = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H₂(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
S . C = H₁(C,S | C) ) ) & ex S being Sequence st
( x2 = last S & dom S = succ A & S . 0 = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H₂(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
S . C = H₁(C,S | C) ) ) holds
x1 = x2 ) ) from ORDINAL2:sch 7();
hence ( ex b₁ being set ex S being Sequence st
( b₁ = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) & ( for b₁, b₂ being set st ex S being Sequence st
( b₁ = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) & ex S being Sequence st
( b₂ = last S & dom S = succ A & S . 0 = card omega & ( for B being Ordinal st succ B in succ A holds
S . (succ B) = nextcard (S . B) ) & ( for B being Ordinal st B in succ A & B <> 0 & B is limit_ordinal holds
S . B = card (sup (S | B)) ) ) holds
b₁ = b₂ ) ) ; :: thesis:

end;

:: deftheorem Def5 defines aleph CARD_1:def 5 :

Lm1: now :: thesis:

deffunc H₁( Ordinal, Sequence) -> Cardinal = card (sup $2);
deffunc H₂( Ordinal, set ) -> Cardinal = nextcard $2;
deffunc H₃( Ordinal) -> set = aleph $1;
A1: for A being Ordinal
for x being object holds
( x = H₃(A) iff ex S being Sequence st
( x = last S & dom S = succ A & S . 0 = card omega & ( for C being Ordinal st succ C in succ A holds
S . (succ C) = H₂(C,S . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
S . C = H₁(C,S | C) ) ) ) by Def5;
H₃( 0 ) = card omega from ORDINAL2:sch 8(A1);
hence aleph 0 = card omega ; :: thesis:
thus for A being Ordinal holds H₃( succ A) = H₂(A,H₃(A)) from ORDINAL2:sch 9(A1); :: thesis:
thus for A being Ordinal st A <> 0 & A is limit_ordinal holds
for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S) :: thesis:

let A be Ordinal; :: thesis:
assume A2: ( A <> 0 & A is limit_ordinal ) ; :: thesis:
let S be Sequence; :: thesis:
assume that
A3: dom S = A and
A4: for B being Ordinal st B in A holds
S . B = H₃(B) ; :: thesis:
thus H₃(A) = H₁(A,S) from ORDINAL2:sch 10(A1, A2, A3, A4); :: thesis:

end;

deffunc H₁( Ordinal) -> set = aleph $1;

registration

let A be Ordinal;

cluster aleph A -> cardinal ;

A1: now :: thesis:

consider S being Sequence such that
A2: ( dom S = A & ( for B being Ordinal st B in A holds
S . B = H₁(B) ) ) from ORDINAL2:sch 2();
assume that
A3: A <> {} and
A4: for B being Ordinal holds A <> succ B ; :: thesis:
aleph A = card (sup S) by A3, A2, Lm1, A4, ORDINAL1:29;
hence aleph A is Cardinal ; :: thesis:

end;

given B being Ordinal such that A5: A = succ B ; :: thesis:
aleph A = nextcard (aleph B) by A5, Lm1;
hence aleph A is cardinal ; :: thesis:

end;

hence aleph A is cardinal by A1, Lm1; :: thesis:

end;

theorem :: CARD_1:19

for A being Ordinal holds aleph (succ A) = nextcard (aleph A) by Lm1;

theorem :: CARD_1:20

for A being Ordinal st A <> {} & A is limit_ordinal holds
for S being Sequence st dom S = A & ( for B being Ordinal st B in A holds
S . B = aleph B ) holds
aleph A = card (sup S) by Lm1;

theorem Th20: :: CARD_1:21

for A, B being Ordinal holds
( A in B iff aleph A in aleph B )

let A, B be Ordinal; :: thesis:
defpred S₁[ Ordinal] means for A being Ordinal st A in $1 holds
aleph A in aleph $1;
A1: for B being Ordinal st S₁[B] holds
S₁[ succ B]

let B be Ordinal; :: thesis:
assume A2: S₁[B] ; :: thesis:
let A be Ordinal; :: thesis:
A3: aleph (succ B) = nextcard (aleph B) by Lm1;

A4: now :: thesis:

assume A in B ; :: thesis:
then A5: aleph A in aleph B by A2;
aleph B in nextcard (aleph B) by Th17;
hence ( A in succ B implies aleph A in aleph (succ B) ) by A3, A5, ORDINAL1:10; :: thesis:

end;

A6: ( A c< B iff ( A c= B & A <> B ) ) ;
assume A in succ B ; :: thesis:
hence aleph A in aleph (succ B) by A3, A6, A4, Th17, ORDINAL1:11, ORDINAL1:22; :: thesis:

end;

A7: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

let B be Ordinal; :: thesis:
assume that
A8: B <> 0 and
A9: B is limit_ordinal and
for C being Ordinal st C in B holds
for A being Ordinal st A in C holds
aleph A in aleph C ; :: thesis:
let A be Ordinal; :: thesis:
consider S being Sequence such that
A10: ( dom S = B & ( for C being Ordinal st C in B holds
S . C = H₁(C) ) ) from ORDINAL2:sch 2();
assume A in B ; :: thesis:
then succ A in B by A9, ORDINAL1:28;
then A11: ( S . (succ A) in rng S & S . (succ A) = aleph (succ A) ) by A10, FUNCT_1:def 3;
sup (rng S) = sup S by ORDINAL2:26;
then A12: aleph (succ A) c= sup S by A11, ORDINAL1:def 2, ORDINAL2:19;
A13: card (aleph (succ A)) = aleph (succ A) ;
A14: ( aleph (succ A) = nextcard (aleph A) & aleph A in nextcard (aleph A) ) by Th17, Lm1;
aleph B = card (sup S) by A8, A9, A10, Lm1;
then aleph (succ A) c= aleph B by A12, A13, Th10;
hence aleph A in aleph B by A14; :: thesis:

end;

A15: S₁[ 0 ] ;
A16: for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A15, A1, A7);
hence ( A in B implies aleph A in aleph B ) ; :: thesis:
assume A17: aleph A in aleph B ; :: thesis:
then A18: aleph A <> aleph B ;
not B in A by A16, A17;
hence A in B by A18, ORDINAL1:14; :: thesis:

end;

theorem Th21: :: CARD_1:22

for A, B being Ordinal st aleph A = aleph B holds
A = B

let A, B be Ordinal; :: thesis:
assume A1: aleph A = aleph B ; :: thesis:

A2: now :: thesis:

assume B in A ; :: thesis:
then aleph B in aleph A by Th20;
hence contradiction by A1; :: thesis:

end;

assume A in B ; :: thesis:
then aleph A in aleph B by Th20;
hence contradiction by A1; :: thesis:

end;

hence A = B by A2, ORDINAL1:14; :: thesis:

end;

theorem :: CARD_1:23

for A, B being Ordinal holds
( A c= B iff aleph A c= aleph B )

let A, B be Ordinal; :: thesis:
A1: ( aleph A c< aleph B iff ( aleph A <> aleph B & aleph A c= aleph B ) ) ;
( A in B iff aleph A in aleph B ) by Th20;
hence ( A c= B iff aleph A c= aleph B ) by A1, Th21, ORDINAL1:11, XBOOLE_0:def 8; :: thesis:

end;

theorem :: CARD_1:24

for X, Y, Z being set st X c= Y & Y c= Z & X,Z are_equipotent holds
( X,Y are_equipotent & Y,Z are_equipotent )

let X, Y, Z be set ; :: thesis:
assume that
A1: ( X c= Y & Y c= Z ) and
A2: X,Z are_equipotent ; :: thesis:
A3: card X = card Z by A2, Th4;
( card X c= card Y & card Y c= card Z ) by A1, Th10;
hence ( X,Y are_equipotent & Y,Z are_equipotent ) by A3, Th4, XBOOLE_0:def 10; :: thesis:

end;

theorem :: CARD_1:25

for X, Y being set st bool Y c= X holds
( card Y in card X & not Y,X are_equipotent )

let X, Y be set ; :: thesis:
assume bool Y c= X ; :: thesis:
then card (bool Y) c= card X by Th10;
hence card Y in card X by Th13; :: thesis:
then card Y <> card X ;
hence not Y,X are_equipotent by Th4; :: thesis:

end;

theorem Th25: :: CARD_1:26

for X being set st X, {} are_equipotent holds
X = {} by RELAT_1:42;

theorem :: CARD_1:27

card {} = 0 ;

theorem Th27: :: CARD_1:28

for X being set
for x being object holds
( X,{x} are_equipotent iff ex x being object st X = {x} )

let X be set ; :: thesis:
let x be object ; :: thesis:
thus ( X,{x} are_equipotent implies ex x being object st X = {x} ) :: thesis:

assume X,{x} are_equipotent ; :: thesis:
then consider f being Function such that
f is one-to-one and
A1: dom f = {x} and
A2: rng f = X by WELLORD2:def 4;
rng f = {(f . x)} by A1, FUNCT_1:4;
hence ex x being object st X = {x} by A2; :: thesis:

end;

given y being object such that A3: X = {y} ; :: thesis:
take f = X --> x; :: according to WELLORD2:def 4 :: thesis:
A4: dom f = X ;
thus f is one-to-one :: thesis:

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A5: a in dom f and
A6: b in dom f and
f . a = f . b ; :: thesis:
a = y by A3, A5, TARSKI:def 1;
hence a = b by A3, A6, TARSKI:def 1; :: thesis:

end;

thus dom f = X ; :: thesis:
thus rng f c= {x} by FUNCOP_1:13; :: according to XBOOLE_0:def 10 :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in {x} ; :: thesis:
then A7: a = x by TARSKI:def 1;
A8: y in {y} by TARSKI:def 1;
then f . y = x by A3, FUNCOP_1:7;
hence a in rng f by A3, A4, A7, A8, FUNCT_1:def 3; :: thesis:

end;

theorem :: CARD_1:29

for X being set
for x being object holds
( card X = card {x} iff ex x being object st X = {x} ) by Th4, Th27;

theorem Th29: :: CARD_1:30

for x being object holds card {x} = 1

let x be object ; :: thesis:
A1: 1 = succ 0 ;
1 is cardinal

take IT = 1; :: according to CARD_1:def 1 :: thesis:
thus 1 = IT ; :: thesis:
let A be Ordinal; :: thesis:
assume A,IT are_equipotent ; :: thesis:
then ex y being object st A = {y} by A1, Th27;
hence IT c= A by A1, ZFMISC_1:33; :: thesis:

end;

then reconsider M = 1 as Cardinal ;
{x},M are_equipotent by A1, Th27;
hence card {x} = 1 by Def2; :: thesis:

end;

theorem Th30: :: CARD_1:31

for X, X1, Y, Y1 being set st X misses X1 & Y misses Y1 & X,Y are_equipotent & X1,Y1 are_equipotent holds
X \/ X1,Y \/ Y1 are_equipotent

let X, X1, Y, Y1 be set ; :: thesis:
assume that
A1: X /\ X1 = {} and
A2: Y /\ Y1 = {} ; :: according to XBOOLE_0:def 7 :: thesis:
given f being Function such that A3: f is one-to-one and
A4: dom f = X and
A5: rng f = Y ; :: according to WELLORD2:def 4 :: thesis:
given g being Function such that A6: g is one-to-one and
A7: dom g = X1 and
A8: rng g = Y1 ; :: according to WELLORD2:def 4 :: thesis:
defpred S₁[ object , object ] means ( ( $1 in X & $2 = f . $1 ) or ( $1 in X1 & $2 = g . $1 ) );
A9: for x being object st x in X \/ X1 holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in X \/ X1 ; :: thesis:
then ( x in X or x in X1 ) by XBOOLE_0:def 3;
hence ex y being object st S₁[x,y] ; :: thesis:

end;

A10: for x, y, z being object st x in X \/ X1 & S₁[x,y] & S₁[x,z] holds
y = z by A1, XBOOLE_0:def 4;
consider h being Function such that
A11: dom h = X \/ X1 and
A12: for x being object st x in X \/ X1 holds
S₁[x,h . x] from FUNCT_1:sch 2(A10, A9);
take h ; :: according to WELLORD2:def 4 :: thesis:
thus h is one-to-one :: thesis:

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A13: x in dom h and
A14: y in dom h and
A15: h . x = h . y ; :: thesis:
A16: ( ( y in X & h . y = f . y ) or ( y in X1 & h . y = g . y ) ) by A11, A12, A14;
A17: ( ( x in X & h . x = f . x ) or ( x in X1 & h . x = g . x ) ) by A11, A12, A13;

A18: now :: thesis:

assume A19: ( y in X & x in X1 ) ; :: thesis:
then ( f . y in Y & g . x in Y1 ) by A4, A5, A7, A8, FUNCT_1:def 3;
hence contradiction by A1, A2, A15, A17, A16, A19, XBOOLE_0:def 4; :: thesis:

end;

assume A20: ( x in X & y in X1 ) ; :: thesis:
then ( f . x in Y & g . y in Y1 ) by A4, A5, A7, A8, FUNCT_1:def 3;
hence contradiction by A1, A2, A15, A17, A16, A20, XBOOLE_0:def 4; :: thesis:

end;

hence x = y by A3, A4, A6, A7, A15, A17, A16, A18; :: thesis:

end;

thus dom h = X \/ X1 by A11; :: thesis:
thus rng h c= Y \/ Y1 :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng h ; :: thesis:
then consider y being object such that
A21: y in dom h and
A22: x = h . y by FUNCT_1:def 3;
A23: ( ( y in X & x = f . y ) or ( y in X1 & x = g . y ) ) by A11, A12, A21, A22;

A24: now :: thesis:

assume y in X1 ; :: thesis:
then x in Y1 by A1, A7, A8, A23, FUNCT_1:def 3, XBOOLE_0:def 4;
hence x in Y \/ Y1 by XBOOLE_0:def 3; :: thesis:

end;

assume y in X ; :: thesis:
then x in Y by A1, A4, A5, A23, FUNCT_1:def 3, XBOOLE_0:def 4;
hence x in Y \/ Y1 by XBOOLE_0:def 3; :: thesis:

end;

hence x in Y \/ Y1 by A11, A21, A24, XBOOLE_0:def 3; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in Y \/ Y1 ; :: thesis:

A26: now :: thesis:

assume x in Y1 ; :: thesis:
then consider y being object such that
A27: y in dom g and
A28: x = g . y by A8, FUNCT_1:def 3;
A29: y in X \/ X1 by A7, A27, XBOOLE_0:def 3;
then S₁[y,h . y] by A12;
hence x in rng h by A1, A7, A11, A27, A28, A29, FUNCT_1:def 3, XBOOLE_0:def 4; :: thesis:

end;

assume x in Y ; :: thesis:
then consider y being object such that
A30: y in dom f and
A31: x = f . y by A5, FUNCT_1:def 3;
A32: y in X \/ X1 by A4, A30, XBOOLE_0:def 3;
then S₁[y,h . y] by A12;
hence x in rng h by A1, A4, A11, A30, A31, A32, FUNCT_1:def 3, XBOOLE_0:def 4; :: thesis:

end;

hence x in rng h by A25, A26, XBOOLE_0:def 3; :: thesis:

end;

theorem Th31: :: CARD_1:32

for X being set
for x, y being object st x in X & y in X holds
X \ {x},X \ {y} are_equipotent

let X be set ; :: thesis:
let x, y be object ; :: thesis:
assume that
A1: x in X and
A2: y in X ; :: thesis:
defpred S₁[ object , object ] means ( ( $1 = y & $2 = x ) or ( $1 <> y & $1 = $2 ) );
A3: for a being object st a in X \ {x} holds
ex b being object st S₁[a,b]

let a be object ; :: thesis:
assume a in X \ {x} ; :: thesis:
( a = y implies ex b being object st S₁[a,b] ) ;
hence ex b being object st S₁[a,b] ; :: thesis:

end;

A4: for a, b1, b2 being object st a in X \ {x} & S₁[a,b1] & S₁[a,b2] holds
b1 = b2 ;
consider f being Function such that
A5: ( dom f = X \ {x} & ( for a being object st a in X \ {x} holds
S₁[a,f . a] ) ) from FUNCT_1:sch 2(A4, A3);
take f ; :: according to WELLORD2:def 4 :: thesis:
thus f is one-to-one :: thesis:

let b1, b2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A6: ( b1 in dom f & b2 in dom f ) and
A7: ( f . b1 = f . b2 & b1 <> b2 ) ; :: thesis:
A8: ( not b1 in {x} & not b2 in {x} ) by A5, A6, XBOOLE_0:def 5;
( S₁[b1,f . b1] & S₁[b2,f . b2] ) by A5, A6;
hence contradiction by A7, A8, TARSKI:def 1; :: thesis:

end;

thus dom f = X \ {x} by A5; :: thesis:
thus rng f c= X \ {y} :: according to XBOOLE_0:def 10 :: thesis:

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng f ; :: thesis:
then consider a being object such that
A9: a in dom f and
A10: z = f . a by FUNCT_1:def 3;

A11: now :: thesis:

assume A12: a = y ; :: thesis:
then ( not y in {x} & z = x ) by A5, A9, A10, XBOOLE_0:def 5;
then y <> z by TARSKI:def 1;
then A13: not z in {y} by TARSKI:def 1;
z in X by A1, A5, A9, A10, A12;
hence z in X \ {y} by A13, XBOOLE_0:def 5; :: thesis:

end;

assume a <> y ; :: thesis:
then ( not a in {y} & a = z ) by A5, A9, A10, TARSKI:def 1;
hence z in X \ {y} by A5, A9, XBOOLE_0:def 5; :: thesis:

end;

hence z in X \ {y} by A11; :: thesis:

end;

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: z in X \ {y} ; :: thesis:
then not z in {y} by XBOOLE_0:def 5;
then A15: z <> y by TARSKI:def 1;

A16: now :: thesis:

assume z <> x ; :: thesis:
then not z in {x} by TARSKI:def 1;
then A17: z in X \ {x} by A14, XBOOLE_0:def 5;
then z = f . z by A5, A15;
hence z in rng f by A5, A17, FUNCT_1:def 3; :: thesis:

end;

assume A18: z = x ; :: thesis:
then not y in {x} by A15, TARSKI:def 1;
then A19: y in dom f by A2, A5, XBOOLE_0:def 5;
then z = f . y by A5, A18;
hence z in rng f by A19, FUNCT_1:def 3; :: thesis:

end;

hence z in rng f by A16; :: thesis:

end;

theorem Th32: :: CARD_1:33

for X being set
for f being Function st X c= dom f & f is one-to-one holds
X,f .: X are_equipotent

let X be set ; :: thesis:
let f be Function; :: thesis:
assume that
A1: X c= dom f and
A2: f is one-to-one ; :: thesis:
take g = f | X; :: according to WELLORD2:def 4 :: thesis:
thus g is one-to-one by A2, FUNCT_1:52; :: thesis:
thus dom g = X by A1, RELAT_1:62; :: thesis:
thus rng g = f .: X by RELAT_1:115; :: thesis:

end;

theorem Th33: :: CARD_1:34

for X, Y being set
for x, y being object st X,Y are_equipotent & x in X & y in Y holds
X \ {x},Y \ {y} are_equipotent

let X, Y be set ; :: thesis:
let x, y be object ; :: thesis:
given f being Function such that A1: f is one-to-one and
A2: dom f = X and
A3: rng f = Y ; :: according to WELLORD2:def 4 :: thesis:
A4: X \ {x},f .: (X \ {x}) are_equipotent by A1, A2, Th32;
assume that
A5: x in X and
A6: y in Y ; :: thesis:
f . x in Y by A2, A3, A5, FUNCT_1:def 3;
then A7: Y \ {(f . x)},Y \ {y} are_equipotent by A6, Th31;
f .: (X \ {x}) = (f .: X) \ (Im (f,x)) by A1, FUNCT_1:64
.= Y \ (Im (f,x)) by A2, A3, RELAT_1:113
.= Y \ {(f . x)} by A2, A5, FUNCT_1:59 ;
hence X \ {x},Y \ {y} are_equipotent by A4, A7, WELLORD2:15; :: thesis:

end;

theorem Th34: :: CARD_1:35

for X, Y being set st succ X, succ Y are_equipotent holds
X,Y are_equipotent

let X, Y be set ; :: thesis:
A1: ( X in succ X & Y in succ Y ) by ORDINAL1:6;
( X = (succ X) \ {X} & Y = (succ Y) \ {Y} ) by ORDINAL1:37;
hence ( succ X, succ Y are_equipotent implies X,Y are_equipotent ) by A1, Th33; :: thesis:

end;

theorem Th35: :: CARD_1:36

for n being Nat holds
( n = {} or ex m being Nat st n = succ m )

let n be Nat; :: thesis:
defpred S₁[ Nat] means ( $1 = {} or ex m being Nat st $1 = succ m );
A1: for a being Nat st S₁[a] holds
S₁[ succ a] ;
A2: S₁[ 0 ] ;
thus S₁[n] from ORDINAL2:sch 17(A2, A1); :: thesis:

end;

Lm2: for m, n being Nat st n,m are_equipotent holds
n = m

let m, n be Nat; :: thesis:
defpred S₁[ Nat] means for n being Nat st n,$1 are_equipotent holds
n = $1;
A1: for a being Nat st S₁[a] holds
S₁[ succ a]

let a be Nat; :: thesis:
assume A2: S₁[a] ; :: thesis:
let n be Nat; :: thesis:
assume A3: n, succ a are_equipotent ; :: thesis:

per cases ;

suppose n = {} ; :: thesis:

hence n = succ a by A3, RELAT_1:42; :: thesis:

end;

suppose n <> {} ; :: thesis:

then ex m being Nat st n = succ m by Th35;
hence n = succ a by A2, A3, Th34; :: thesis:

end;

A4: S₁[ 0 ] by Th25;
S₁[m] from ORDINAL2:sch 17(A4, A1);
hence ( n,m are_equipotent implies n = m ) ; :: thesis:

end;

theorem Th36: :: CARD_1:37

for x being object st x in omega holds
x is cardinal

let x be object ; :: thesis:
assume that
A1: x in omega and
A2: for B being Ordinal st x = B holds
ex C being Ordinal st
( C,B are_equipotent & not B c= C ) ; :: according to CARD_1:def 1 :: thesis:
reconsider A = x as Ordinal by A1;
consider B being Ordinal such that
A3: B,A are_equipotent and
A4: not A c= B by A2;
B in A by A4, ORDINAL1:16;
then B in omega by A1, ORDINAL1:10;
then reconsider n = A, m = B as Nat by A1;
n,m are_equipotent by A3;
hence contradiction by A4, Lm2; :: thesis:

end;

registration

cluster natural -> cardinal for number ;

correctness by Th36;

end;

theorem Th37: :: CARD_1:38

for X, Y being set st X,Y are_equipotent & X is finite holds
Y is finite

let X, Y be set ; :: thesis:
assume X,Y are_equipotent ; :: thesis:
then consider f being Function such that
f is one-to-one and
A1: dom f = X and
A2: rng f = Y ;
given p being Function such that A3: rng p = X and
A4: dom p in omega ; :: according to FINSET_1:def 1 :: thesis:
take f * p ; :: according to FINSET_1:def 1 :: thesis:
thus rng (f * p) = Y by A1, A2, A3, RELAT_1:28; :: thesis:
thus dom (f * p) in omega by A1, A3, A4, RELAT_1:27; :: thesis:

end;

theorem Th38: :: CARD_1:39

for n being Nat holds
( n is finite & card n is finite )

let n be Nat; :: thesis:
reconsider n = n as Element of omega by ORDINAL1:def 12;
( rng (id n) = n & dom (id n) = n ) by RELAT_1:45;
hence ( n is finite & card n is finite ) ; :: thesis:

end;

theorem :: CARD_1:40

for m, n being Nat st card n = card m holds
n = m ;

theorem :: CARD_1:41

for m, n being Nat holds
( card n c= card m iff n c= m ) ;

theorem :: CARD_1:42

for m, n being Nat holds
( card n in card m iff n in m ) ;

Lm3: for X being set st X is finite holds
ex n being Nat st X,n are_equipotent

let X be set ; :: thesis:
defpred S₁[ set ] means ex n being Nat st $1,n are_equipotent ;
A1: S₁[ {} ] ;
A2: for Z, Y being set st Z in X & Y c= X & S₁[Y] holds
S₁[Y \/ {Z}]

let Z, Y be set ; :: thesis:
assume that
Z in X and
Y c= X ; :: thesis:
given n being Nat such that A3: Y,n are_equipotent ; :: thesis:
A4: ( not Z in Y implies S₁[Y \/ {Z}] )

assume A5: not Z in Y ; :: thesis:

set x = the Element of Y /\ {Z};
assume Y /\ {Z} <> {} ; :: thesis:
then ( the Element of Y /\ {Z} in Y & the Element of Y /\ {Z} in {Z} ) by XBOOLE_0:def 4;
hence contradiction by A5, TARSKI:def 1; :: thesis:

end;

then A6: Y misses {Z} ;

A7: now :: thesis:

assume n meets {n} ; :: thesis:
then consider x being object such that
A8: x in n and
A9: x in {n} by XBOOLE_0:3;
A: x = n by A9, TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx ;
hence contradiction by A8, A; :: thesis:

end;

take succ n ; :: thesis:
{Z},{n} are_equipotent by Th27;
hence Y \/ {Z}, succ n are_equipotent by A3, A7, A6, Th30; :: thesis:

end;

( Z in Y implies S₁[Y \/ {Z}] )

assume A10: Z in Y ; :: thesis:
take n ; :: thesis:
thus Y \/ {Z},n are_equipotent by A3, A10, XBOOLE_1:12, ZFMISC_1:31; :: thesis:

end;

hence S₁[Y \/ {Z}] by A4; :: thesis:

end;

assume A11: X is finite ; :: thesis:
thus S₁[X] from FINSET_1:sch 2(A11, A1, A2); :: thesis:

end;

theorem :: CARD_1:43

canceled;

theorem Th42: :: CARD_1:44

for n being Nat holds nextcard (card n) = card (succ n)

let n be Nat; :: thesis:
reconsider sn = succ n as Nat ;
for M being Cardinal st card (card n) in M holds
card (succ n) c= M by ORDINAL1:21;
hence nextcard (card n) = card (succ n) by Def3, ORDINAL1:6; :: thesis:

end;

definition

let X be finite set ;
:: original: card
redefine func card X -> Element of omega ;
coherence

consider n being Nat such that
A1: X,n are_equipotent by Lm3;
reconsider n = n as Element of omega by ORDINAL1:def 12;
X,n are_equipotent by A1;
hence card X is Element of omega by Def2; :: thesis:

end;

theorem :: CARD_1:45

for X being set st X is finite holds
nextcard X is finite

let X be set ; :: thesis:
assume X is finite ; :: thesis:
then reconsider X = X as finite set ;
card X = card (card X) ;
then A1: card (succ (card X)) = nextcard (card X) by Th42;
nextcard (card X) = nextcard X by Def2, Th16;
hence nextcard X is finite by A1, Th38; :: thesis:

end;

scheme :: CARD_1:sch 1
CardinalInd{ P₁[ set ] } :

for M being Cardinal holds P₁[M]

provided

A1: P₁[ {} ] and
A2: for M being Cardinal st P₁[M] holds
P₁[ nextcard M] and
A3: for M being Cardinal st M <> {} & M is limit_cardinal & ( for N being Cardinal st N in M holds
P₁[N] ) holds
P₁[M]

let M be Cardinal; :: thesis:
defpred S₁[ Ordinal] means ( $1 is Cardinal implies P₁[$1] );
A4: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

let A be Ordinal; :: thesis:
assume that
A5: for B being Ordinal st B in A holds
S₁[B] and
A6: A is Cardinal ; :: thesis:
reconsider M = A as Cardinal by A6;

A7: now :: thesis:

assume not M is limit_cardinal ; :: thesis:
then consider N being Cardinal such that
A8: M = nextcard N ;
N in M by A8, Th17;
hence P₁[M] by A2, A5, A8; :: thesis:

end;

assume A9: ( M <> {} & M is limit_cardinal ) ; :: thesis:
for N being Cardinal st N in M holds
P₁[N] by A5;
hence P₁[M] by A3, A9; :: thesis:

end;

hence P₁[A] by A1, A7; :: thesis:

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A4);
hence P₁[M] ; :: thesis:

end;

scheme :: CARD_1:sch 2
CardinalCompInd{ P₁[ set ] } :

for M being Cardinal holds P₁[M]

provided

A1: for M being Cardinal st ( for N being Cardinal st N in M holds
P₁[N] ) holds
P₁[M]

let M be Cardinal; :: thesis:
defpred S₁[ Ordinal] means ( $1 is Cardinal implies P₁[$1] );
A2: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

let A be Ordinal; :: thesis:
assume A3: for B being Ordinal st B in A & B is Cardinal holds
P₁[B] ; :: thesis:
assume A is Cardinal ; :: thesis:
then reconsider M = A as Cardinal ;
for N being Cardinal st N in M holds
P₁[N] by A3;
hence P₁[A] by A1; :: thesis:

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A2);
hence P₁[M] ; :: thesis:

end;

theorem Th44: :: CARD_1:46

aleph 0 = omega

thus aleph 0 c= omega by Lm1, Th7; :: according to XBOOLE_0:def 10 :: thesis:
thus omega c= aleph 0 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in omega ; :: thesis:
then reconsider A = x as Ordinal ;
consider n being Element of omega such that
A2: A = n by A1;
card (succ n) c= card omega by Th10, ORDINAL1:21;
hence x in aleph 0 by A2, Lm1, ORDINAL1:6; :: thesis:

end;

registration

cluster omega -> cardinal for number ;

coherence by Th44;

end;

theorem :: CARD_1:47

card omega = omega ;

registration

cluster omega -> limit_cardinal ;

given N being Cardinal such that A1: omega = nextcard N ; :: according to CARD_1:def 4 :: thesis:
N in omega by A1, Th17;
then A2: succ N in omega by ORDINAL1:def 12;
reconsider n = N as Element of omega by A1, Th17;
( nextcard (card n) = card (succ n) & card n = n ) by Th42;
hence contradiction by A1, A2; :: thesis:

end;

registration

cluster -> finite for Element of omega ;

coherence by Th38;

end;

registration

cluster epsilon-transitive epsilon-connected ordinal finite cardinal for Cardinal;

set n = the Element of omega ;
take the Element of omega ; :: thesis:
thus the Element of omega is finite ; :: thesis:

end;

theorem :: CARD_1:48

for M being finite Cardinal ex n being Nat st M = card n

let M be finite Cardinal; :: thesis:
card M = M ;
hence ex n being Nat st M = card n ; :: thesis:

end;

registration

let X be finite set ;

cluster (X) -> finite ;

end;

Lm4: for A being Ordinal
for n being Nat st A,n are_equipotent holds
A = n

let A be Ordinal; :: thesis:
let n be Nat; :: thesis:
defpred S₁[ Nat] means for A being Ordinal st A,$1 are_equipotent holds
A = $1;
A1: for n being Nat st S₁[n] holds
S₁[ succ n]

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
let A be Ordinal; :: thesis:
A3: ( n in succ n & (succ n) \ {n} = n ) by ORDINAL1:6, ORDINAL1:37;
assume A4: A, succ n are_equipotent ; :: thesis:
then A <> {} by RELAT_1:42;
then A5: {} in A by ORDINAL3:8;

A6: succ n in omega by ORDINAL1:def 12;
assume A is limit_ordinal ; :: thesis:
then A7: omega c= A by A5, ORDINAL1:def 11;
card A = card (succ n) by A4, Th4;
hence contradiction by A7, Lm1, Th10, ORDINAL1:5, A6; :: thesis:

end;

then consider B being Ordinal such that
A8: A = succ B by ORDINAL1:29;
( B in A & A \ {B} = B ) by A8, ORDINAL1:6, ORDINAL1:37;
hence A = succ n by A2, A4, A8, A3, Th33; :: thesis:

end;

A9: S₁[ 0 ] by Th25;
S₁[n] from ORDINAL2:sch 17(A9, A1);
hence ( A,n are_equipotent implies A = n ) ; :: thesis:

end;

Lm5: for A being Ordinal holds
( A is finite iff A in omega )

let A be Ordinal; :: thesis:
thus ( A is finite implies A in omega ) :: thesis:

assume A is finite ; :: thesis:
then consider n being Nat such that
A1: A,n are_equipotent by Lm3;
A = n by A1, Lm4;
hence A in omega by ORDINAL1:def 12; :: thesis:

end;

assume A in omega ; :: thesis:
hence A is finite ; :: thesis:

end;

registration

cluster omega -> infinite ;

not omega in omega ;
hence not omega is finite by Lm5; :: thesis:

end;

registration

cluster infinite for set ;

take omega ; :: thesis:
thus omega is infinite ; :: thesis:

end;

registration

let X be infinite set ;

cluster card X -> infinite ;

X, card X are_equipotent by Def2;
hence not card X is finite by Th37; :: thesis:

end;

theorem Th47: :: CARD_1:49

1 = {0}

thus 1 = succ 0
.= {0} ; :: thesis:

end;

theorem Th48: :: CARD_1:50

2 = {0,1}

thus 2 = succ 1
.= {0,1} by Th47, ENUMSET1:1 ; :: thesis:

end;

theorem Th49: :: CARD_1:51

3 = {0,1,2}

thus 3 = succ 2
.= {0,1,2} by Th48, ENUMSET1:3 ; :: thesis:

end;

theorem Th50: :: CARD_1:52

4 = {0,1,2,3}

thus 4 = succ 3
.= {0,1,2,3} by Th49, ENUMSET1:6 ; :: thesis:

end;

theorem Th51: :: CARD_1:53

5 = {0,1,2,3,4}

thus 5 = succ 4
.= {0,1,2,3,4} by Th50, ENUMSET1:10 ; :: thesis:

end;

theorem Th52: :: CARD_1:54

6 = {0,1,2,3,4,5}

thus 6 = succ 5
.= {0,1,2,3,4,5} by Th51, ENUMSET1:15 ; :: thesis:

end;

theorem Th53: :: CARD_1:55

7 = {0,1,2,3,4,5,6}

thus 7 = succ 6
.= {0,1,2,3,4,5,6} by Th52, ENUMSET1:21 ; :: thesis:

end;

theorem Th54: :: CARD_1:56

8 = {0,1,2,3,4,5,6,7}

thus 8 = succ 7
.= {0,1,2,3,4,5,6,7} by Th53, ENUMSET1:28 ; :: thesis:

end;

theorem Th55: :: CARD_1:57

9 = {0,1,2,3,4,5,6,7,8}

thus 9 = succ 8
.= {0,1,2,3,4,5,6,7,8} by Th54, ENUMSET1:84 ; :: thesis:

end;

theorem :: CARD_1:58

10 = {0,1,2,3,4,5,6,7,8,9}

thus 10 = succ 9
.= {0,1,2,3,4,5,6,7,8,9} by Th55, ENUMSET1:85 ; :: thesis:

end;

theorem :: CARD_1:59

for f being Function st dom f is infinite & f is one-to-one holds
rng f is infinite

let f be Function; :: thesis:
assume that
A1: dom f is infinite and
A2: f is one-to-one ; :: thesis:
dom f, rng f are_equipotent by A2;
hence rng f is infinite by A1, Th37; :: thesis:

end;

registration

cluster natural non zero for object ;

take 1 ; :: thesis:
thus ( not 1 is zero & 1 is natural ) ; :: thesis:

end;

cluster epsilon-transitive epsilon-connected ordinal natural non zero cardinal for Nat;

take 1 ; :: thesis:
thus not 1 is zero ; :: thesis:

end;

registration

let n be natural non zero Number ;

cluster Segm n -> non empty ;

n <> 0 ;
hence not Segm n is empty ; :: thesis:

end;

definition

let n be natural Number ;
:: original: Segm
redefine func Segm n -> Subset of omega;
coherence

reconsider n = n as Nat by TARSKI:1;
n in omega by ORDINAL1:def 12;
hence Segm n is Subset of omega by ORDINAL1:16; :: thesis:

end;

theorem :: CARD_1:60

for A being Ordinal
for n being Nat st A,n are_equipotent holds
A = n by Lm4;

theorem :: CARD_1:61

for A being Ordinal holds
( A is finite iff A in omega ) by Lm5;

registration

cluster natural -> finite for set ;

end;

registration

let A be infinite set ;

cluster bool A -> infinite ;

defpred S₁[ object ] means ex y being object st A = {y};
consider X being set such that
A1: for x being object holds
( x in X iff ( x in bool A & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being object holds
( x in union X iff x in A )

let x be object ; :: thesis:
thus ( x in union X implies x in A ) :: thesis:

assume x in union X ; :: thesis:
then consider B being set such that
A2: x in B and
A3: B in X by TARSKI:def 4;
B in bool A by A1, A3;
hence x in A by A2; :: thesis:

end;

assume x in A ; :: thesis:
then {x} c= A by ZFMISC_1:31;
then A4: {x} in X by A1;
x in {x} by TARSKI:def 1;
hence x in union X by A4, TARSKI:def 4; :: thesis:

end;

then A5: union X = A by TARSKI:2;
A6: for B being set st B in X holds
B is finite

let B be set ; :: thesis:
assume B in X ; :: thesis:
then ex y being object st B = {y} by A1;
hence B is finite ; :: thesis:

end;

A7: X c= bool A by A1;
assume bool A is finite ; :: thesis:
hence contradiction by A5, A6, A7, FINSET_1:7; :: thesis:

end;

let B be non empty set ;

cluster [:A,B:] -> infinite ;

deffunc H₂( object ) -> object = A `1 ;
consider f being Function such that
A8: dom f = [:A,B:] and
A9: for x being object st x in [:A,B:] holds
f . x = H₂(x) from FUNCT_1:sch 3();
for x being object holds
( x in rng f iff x in A )

let x be object ; :: thesis:
thus ( x in rng f implies x in A ) :: thesis:

assume x in rng f ; :: thesis:
then consider y being object such that
A10: y in dom f and
A11: f . y = x by FUNCT_1:def 3;
x = y `1 by A8, A9, A10, A11;
hence x in A by A8, A10, MCART_1:10; :: thesis:

end;

set y = the Element of B;
assume A12: x in A ; :: thesis:
then A13: [x, the Element of B] in dom f by A8, ZFMISC_1:87;
f . [x, the Element of B] = [x, the Element of B] `1 by A9, A12, ZFMISC_1:87
.= x ;
hence x in rng f by A13, FUNCT_1:def 3; :: thesis:

end;

then rng f = A by TARSKI:2;
then A14: f .: [:A,B:] = A by A8, RELAT_1:113;
assume [:A,B:] is finite ; :: thesis:
hence contradiction by A14; :: thesis:

end;

cluster [:B,A:] -> infinite ;

deffunc H₂( object ) -> object = A `2 ;
consider f being Function such that
A15: dom f = [:B,A:] and
A16: for x being object st x in [:B,A:] holds
f . x = H₂(x) from FUNCT_1:sch 3();
for y being object holds
( y in rng f iff y in A )

let y be object ; :: thesis:
thus ( y in rng f implies y in A ) :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A17: x in dom f and
A18: f . x = y by FUNCT_1:def 3;
y = x `2 by A15, A16, A17, A18;
hence y in A by A15, A17, MCART_1:10; :: thesis:

end;

set x = the Element of B;
assume A19: y in A ; :: thesis:
then A20: [ the Element of B,y] in dom f by A15, ZFMISC_1:87;
[ the Element of B,y] `2 = y ;
then f . [ the Element of B,y] = y by A16, A19, ZFMISC_1:87;
hence y in rng f by A20, FUNCT_1:def 3; :: thesis:

end;

then rng f = A by TARSKI:2;
then A21: f .: [:B,A:] = A by A15, RELAT_1:113;
assume [:B,A:] is finite ; :: thesis:
hence contradiction by A21; :: thesis:

end;

registration

let X be infinite set ;

cluster infinite for Subset of X;

X c= X ;
hence ex b₁ being Subset of X st b₁ is infinite ; :: thesis:

end;

registration

cluster ordinal finite -> natural for number ;

coherence by Lm5;

end;

theorem Th60: :: CARD_1:62

for f being Function holds card f = card (dom f)

let f be Function; :: thesis:
dom f,f are_equipotent

deffunc H₂( object ) -> object = [$1,(f . $1)];
consider g being Function such that
A1: dom g = dom f and
A2: for x being object st x in dom f holds
g . x = H₂(x) from FUNCT_1:sch 3();
take g ; :: according to WELLORD2:def 4 :: thesis:
thus g is one-to-one :: thesis:

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A3: x in dom g and
A4: y in dom g ; :: thesis:
assume g . x = g . y ; :: thesis:
then [x,(f . x)] = g . y by A1, A2, A3
.= [y,(f . y)] by A1, A2, A4 ;
hence x = y by XTUPLE_0:1; :: thesis:

end;

thus dom g = dom f by A1; :: thesis:
thus rng g c= f :: according to XBOOLE_0:def 10 :: thesis:

let i be object ; :: according to TARSKI:def 3 :: thesis:
assume i in rng g ; :: thesis:
then consider x being object such that
A5: x in dom g and
A6: g . x = i by FUNCT_1:def 3;
g . x = [x,(f . x)] by A1, A2, A5;
hence i in f by A1, A5, A6, FUNCT_1:1; :: thesis:

end;

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A7: [x,y] in f ; :: thesis:
then A8: x in dom f by FUNCT_1:1;
y = f . x by A7, FUNCT_1:1;
then g . x = [x,y] by A2, A7, FUNCT_1:1;
hence [x,y] in rng g by A1, A8, FUNCT_1:def 3; :: thesis:

end;

hence card f = card (dom f) by Th4; :: thesis:

end;

registration

let X be finite set ;

cluster RelIncl X -> finite ;

RelIncl X c= [:X,X:] by WELLORD2:23;
hence RelIncl X is finite ; :: thesis:

end;

theorem :: CARD_1:63

for X being set st RelIncl X is finite holds
X is finite

let X be set ; :: thesis:
set R = RelIncl X;
assume RelIncl X is finite ; :: thesis:
then reconsider A = RelIncl X as finite Relation ;
field A is finite ;
hence X is finite by WELLORD2:def 1; :: thesis:

end;

theorem :: CARD_1:64

for x being object
for k being Nat holds card (k --> x) = k

let x be object ; :: thesis:
let k be Nat; :: thesis:
dom (k --> x) = k ;
hence card (k --> x) = card k by Th60
.= k ;
:: thesis:

end;

definition

let N be object ;
let X be set ;

attr X is N -element means :Def6: :: CARD_1:def 7
card X = N;

end;

:: deftheorem CARD_1:def 6 :

:: deftheorem Def6 defines -element CARD_1:def 7 :

registration

let N be Cardinal;

cluster N -element for set ;

take N ; :: thesis:
thus card N = N ; :: according to CARD_1:def 7 :: thesis:

end;

registration

cluster 0 -element -> empty for set ;

coherence ;

cluster empty -> 0 -element for set ;

end;

registration

let x be object ;

cluster {x} -> 1 -element ;

1 = succ 0 ;
hence card {x} = 1 by Def2, Th27; :: according to CARD_1:def 7 :: thesis:

end;

registration

let N be Cardinal;

cluster Relation-like Function-like N -element for Function;

take f = N --> {{}}; :: thesis:
card (dom f) = N ;
hence card f = N by Th60; :: according to CARD_1:def 7 :: thesis:

end;

registration

let N be Cardinal;
let f be N -element Function;

cluster dom f -> N -element ;

card f = N by Def6;
hence card (dom f) = N by Th60; :: according to CARD_1:def 7 :: thesis:

end;

registration

cluster 1 -element -> non empty trivial for set ;

let X be set ; :: thesis:
assume X is 1 -element ; :: thesis:
then card X = 1
.= card {0} by Th29 ;
then ex x being object st X = {x} by Th4, Th27;
hence ( X is trivial & not X is empty ) ; :: thesis:

end;

cluster non empty trivial -> 1 -element for set ;

let X be set ; :: thesis:
assume ( X is trivial & not X is empty ) ; :: thesis:
then ex x being object st X = {x} by ZFMISC_1:131;
hence X is 1 -element ; :: thesis:

end;

registration

let X be non empty set ;

cluster 1 -element for Subset of X;

take the non empty trivial Subset of X ; :: thesis:
thus the non empty trivial Subset of X is 1 -element ; :: thesis:

end;

definition

let X be non empty set ;
mode Singleton of X is 1 -element Subset of X;

end;

theorem Th63: :: CARD_1:65

for X being non empty set
for A being Singleton of X ex x being Element of X st A = {x}

let X be non empty set ; :: thesis:
let A be Singleton of X; :: thesis:
consider x being object such that
A1: A = {x} by ZFMISC_1:131;
x in A by A1, TARSKI:def 1;
then reconsider x = x as Element of X ;
take x ; :: thesis:
thus A = {x} by A1; :: thesis:

end;

theorem Th64: :: CARD_1:66

for X, Y being set holds
( card X c= card Y iff ex f being Function st X c= f .: Y )

let X, Y be set ; :: thesis:
deffunc H₂( object ) -> object = $1;
thus ( card X c= card Y implies ex f being Function st X c= f .: Y ) :: thesis:

assume card X c= card Y ; :: thesis:
then consider f being Function such that
A1: ( dom f = Y & X c= rng f ) by Th11;
take f ; :: thesis:
thus X c= f .: Y by A1, RELAT_1:113; :: thesis:

end;

given f being Function such that A2: X c= f .: Y ; :: thesis:
defpred S₁[ object ] means $1 in dom f;
deffunc H₃( object ) -> set = f . $1;
consider g being Function such that
A3: ( dom g = Y & ( for x being object st x in Y holds
( ( S₁[x] implies g . x = H₃(x) ) & ( not S₁[x] implies g . x = H₂(x) ) ) ) ) from PARTFUN1:sch 1();
X c= rng g

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then consider y being object such that
A4: y in dom f and
A5: y in Y and
A6: x = f . y by A2, FUNCT_1:def 6;
x = g . y by A3, A4, A5, A6;
hence x in rng g by A3, A5, FUNCT_1:def 3; :: thesis:

end;

hence card X c= card Y by A3, Th11; :: thesis:

end;

theorem :: CARD_1:67

for X being set
for f being Function holds card (f .: X) c= card X by Th64;

theorem :: CARD_1:68

for X, Y being set st card X in card Y holds
Y \ X <> {}

let X, Y be set ; :: thesis:
assume that
A1: card X in card Y and
A2: Y \ X = {} ; :: thesis:
Y c= X by A2, XBOOLE_1:37;
hence contradiction by A1, Th10, ORDINAL1:5; :: thesis:

end;

theorem :: CARD_1:69

for X being set
for x being object holds
( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )

let X be set ; :: thesis:
let x be object ; :: thesis:
deffunc H₂( object ) -> object = [$1,x];
consider f being Function such that
A1: ( dom f = X & ( for y being object st y in X holds
f . y = H₂(y) ) ) from FUNCT_1:sch 3();
thus X,[:X,{x}:] are_equipotent :: thesis:

take f ; :: according to WELLORD2:def 4 :: thesis:
thus f is one-to-one :: thesis:

let y, z be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A2: ( y in dom f & z in dom f ) and
A3: f . y = f . z ; :: thesis:
A4: ( [y,x] `1 = y & [z,x] `1 = z ) ;
( f . y = [y,x] & f . z = [z,x] ) by A1, A2;
hence y = z by A3, A4; :: thesis:

end;

thus dom f = X by A1; :: thesis:
thus rng f c= [:X,{x}:] :: according to XBOOLE_0:def 10 :: thesis: