:: CARD_1 semantic presentation

E1: for b₁, b₂ being Ordinal holds
( b₁ c= b₂ implies succ b₁ c= succ b₂ )

proof

let c₁, c₂ be Ordinal;
assume E2: c₁ c= c₂ ;
let c₃ be set ; :: uses TARSKI:def 3
assume c₃ in succ c₁ ;
then E3: ( c₃ in c₁ or c₃ = c₁ ) by ORDINAL1:13;
c₂ in succ c₂ by ORDINAL1:10;
then ( ( c₃ in c₂ or c₃ in succ c₂ ) & c₂ c= succ c₂ ) by E2, E3, ORDINAL1:22;
hence c₃ <` succ c₂ ;

end;

definition

let c₁ be set ;
attr a₁ is cardinal means :E2: :: CARD_1:def 1
ex b₁ being Ordinal st
( a₁ = b₁ & for b₂ being Ordinal holds
( b₂,b₁ are_equipotent implies b₁ c= b₂ ) );

end;

:: deftheorem E2 defines cardinal CARD_1:def 1 :

registration

cluster cardinal set ;
existence

proof

consider c₁ being Ordinal;
defpred S₁[ Ordinal] means a₁,c₁ are_equipotent ;
E3: ex b₁ being Ordinal st
S₁[b₁] ;
consider c₂ being Ordinal such that
E4: ( S₁[c₂] & for b₁ being Ordinal holds
( S₁[b₁] implies c₂ c= b₁ ) ) from ORDINAL1:sch 1(E3);
reconsider c₃ = c₂ as set ;
take c₃ ;
take c₂ ; :: uses CARD_1:def 1
thus c₃ = c₂ ;
let c₄ be Ordinal;
assume c₄,c₂ are_equipotent ;
then c₄,c₁ are_equipotent by E4, WELLORD2:22;
hence c₂ c= c₄ by E4;

end;

definition

mode Cardinal is cardinal set ;

end;

registration

cluster cardinal -> ordinal set ;
coherence

proof

let c₁ be set ;
assume c₁ is cardinal ;
then ex b₁ being Ordinal st
( c₁ = b₁ & for b₂ being Ordinal holds
( b₂,b₁ are_equipotent implies b₁ c= b₂ ) ) by E2;
hence c₁ is ordinal ;

end;

theorem :: CARD_1:1

canceled;

theorem :: CARD_1:2

canceled;

theorem :: CARD_1:3

canceled;

theorem E3: :: CARD_1:4

for b₁ being set holds
ex b₂ being Ordinal st b₁,b₂ are_equipotent

proof

let c₁ be set ;
consider c₂ being Relation such that
E4: c₂ well_orders c₁ by WELLORD2:26;
set c₃ = c₂ |_2 c₁;
E5: ( field (c₂ |_2 c₁) = c₁ & c₂ |_2 c₁ is well-ordering ) by E4, WELLORD2:25;
take c₄ = order_type_of (c₂ |_2 c₁);
c₂ |_2 c₁, RelIncl c₄ are_isomorphic by E5, WELLORD2:def 2;
then consider c₅ being Function such that
E6: c₅ is_isomorphism_of c₂ |_2 c₁, RelIncl c₄ by WELLORD1:def 8;
E7: ( dom c₅ = field (c₂ |_2 c₁) & rng c₅ = field (RelIncl c₄) & c₅ is one-to-one & for b₁, b₂ being set holds
( [b₁,b₂] in c₂ |_2 c₁ iff ( b₁ in field (c₂ |_2 c₁) & b₂ in field (c₂ |_2 c₁) & [(c₅ . b₁),(c₅ . b₂)] in RelIncl c₄ ) ) ) by E6, WELLORD1:def 7;
take c₅ ; :: uses WELLORD2:def 4
thus ( c₅ is one-to-one & dom c₅ = c₁ & rng c₅ = c₄ ) by E4, E7, WELLORD2:25, WELLORD2:def 1;

end;

notation

let c₁, c₂ be Cardinal;

end;

theorem :: CARD_1:5

canceled;

theorem :: CARD_1:6

canceled;

theorem :: CARD_1:7

canceled;

theorem E4: :: CARD_1:8

for b₁, b₂ being Cardinal holds
( b₁ = b₂ iff b₁,b₂ are_equipotent )

proof

let c₁, c₂ be Cardinal;
thus ( c₁ = c₂ implies c₁,c₂ are_equipotent ) ;
consider c₃ being Ordinal such that
E5: ( c₁ = c₃ & for b₁ being Ordinal holds
( b₁,c₃ are_equipotent implies c₃ c= b₁ ) ) by E2;
consider c₄ being Ordinal such that
E6: ( c₂ = c₄ & for b₁ being Ordinal holds
( b₁,c₄ are_equipotent implies c₄ c= b₁ ) ) by E2;
assume E7: c₁,c₂ are_equipotent ;
then E8: ( c₄ c= c₃ & c₂,c₁ are_equipotent ) by E5, E6;
c₃ c= c₄ by E5, E6, E7;
hence c₁ = c₂ by E5, E6, E8, XBOOLE_0:def 10;

end;

theorem :: CARD_1:9

canceled;

theorem :: CARD_1:10

canceled;

theorem :: CARD_1:11

canceled;

theorem :: CARD_1:12

canceled;

theorem :: CARD_1:13

for b₁, b₂ being Cardinal holds
( b₁ <` b₂ iff ( b₁ <=` b₂ & b₁ <> b₂ ) )

proof

let c₁, c₂ be Cardinal;
( c₁ c< c₂ iff ( c₁ c= c₂ & c₁ <> c₂ ) ) by XBOOLE_0:def 8;
hence ( c₁ <` c₂ iff ( c₁ <=` c₂ & c₁ <> c₂ ) ) by ORDINAL1:21, ORDINAL1:def 2;

end;

theorem :: CARD_1:14

for b₁, b₂ being Cardinal holds
( b₁ <` b₂ iff not b₂ <=` b₁ ) by ORDINAL1:7, ORDINAL1:26;

definition

let c₁ be set ;
canceled;
canceled;
canceled;
func Card a₁ -> Cardinal means :E5: :: CARD_1:def 5
a₁,a₂ are_equipotent ;
existence

proof

defpred S₁[ Ordinal] means a₁,c₁ are_equipotent ;
E5: ex b₁ being Ordinal st
S₁[b₁] by E3;
consider c₂ being Ordinal such that
E6: ( S₁[c₂] & for b₁ being Ordinal holds
( S₁[b₁] implies c₂ c= b₁ ) ) from ORDINAL1:sch 1(E5);
c₂ is cardinal

proof

take c₂ ; :: uses CARD_1:def 1
thus c₂ = c₂ ;
let c₃ be Ordinal;
assume c₃,c₂ are_equipotent ;
then c₁,c₃ are_equipotent by E6, WELLORD2:22;
hence c₂ c= c₃ by E6;

end;

then reconsider c₃ = c₂ as Cardinal ;
take c₃ ;
thus c₁,c₃ are_equipotent by E6;

end;

uniqueness

proof

let c₂, c₃ be Cardinal;
assume that E5: c₁,c₂ are_equipotent
and E6: c₁,c₃ are_equipotent ;
c₂,c₃ are_equipotent by E5, E6, WELLORD2:22;
hence c₂ = c₃ by E4;

end;

:: deftheorem CARD_1:def 2 :

:: deftheorem CARD_1:def 3 :

:: deftheorem CARD_1:def 4 :

:: deftheorem E5 defines Card CARD_1:def 5 :

theorem :: CARD_1:15

canceled;

theorem :: CARD_1:16

canceled;

theorem :: CARD_1:17

canceled;

theorem :: CARD_1:18

canceled;

theorem :: CARD_1:19

canceled;

theorem :: CARD_1:20

canceled;

theorem E6: :: CARD_1:21

for b₁, b₂ being set holds
( b₁,b₂ are_equipotent iff Card b₁ = Card b₂ )

proof

let c₁, c₂ be set ;
E7: ( c₁, Card c₁ are_equipotent & c₂, Card c₂ are_equipotent ) by E5;
thus ( c₁,c₂ are_equipotent implies Card c₁ = Card c₂ )

proof

assume c₁,c₂ are_equipotent ;
then Card c₁,c₂ are_equipotent by E7, WELLORD2:22;
hence Card c₁ = Card c₂ by E5;

end;

assume Card c₁ = Card c₂ ;
hence c₁,c₂ are_equipotent by E7, WELLORD2:22;

end;

theorem E7: :: CARD_1:22

for b₁ being Relation holds
( b₁ is well-ordering implies field b₁, order_type_of b₁ are_equipotent )

proof

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

end;

theorem E8: :: CARD_1:23

for b₁ being set
for b₂ being Cardinal holds
( b₁ c= b₂ implies Card b₁ <=` b₂ )

proof

let c₁ be set ;
let c₂ be Cardinal;
defpred S₁[ Ordinal] means ( a₁ c= c₂ & c₁,a₁ are_equipotent );
reconsider c₃ = c₂ as Ordinal ;
assume c₁ c= c₂ ;
then E9: ( order_type_of (RelIncl c₁) c= c₃ & RelIncl c₁ is well-ordering & field (RelIncl c₁) = c₁ ) by WELLORD2:9, WELLORD2:17, WELLORD2:def 1;
then c₁, order_type_of (RelIncl c₁) are_equipotent by E7;
then E10: ex b₁ being Ordinal st
S₁[b₁] by E9;
consider c₄ being Ordinal such that
E11: ( S₁[c₄] & for b₁ being Ordinal holds
( S₁[b₁] implies c₄ c= b₁ ) ) from ORDINAL1:sch 1(E10);
c₄ is cardinal

proof

take c₄ ; :: uses CARD_1:def 1
thus c₄ = c₄ ;
let c₅ be Ordinal;
assume c₅,c₄ are_equipotent ;
then E12: c₁,c₅ are_equipotent by E11, WELLORD2:22;
assume E13: not c₄ c= c₅ ;
then c₃ c= c₅ by E11, E12;
hence not verum by E11, E13, XBOOLE_1:1;

end;

then reconsider c₅ = c₄ as Cardinal ;
Card c₁ = c₅ by E11, E5;
hence Card c₁ c= c₂ by E11;

end;

theorem E9: :: CARD_1:24

for b₁ being Ordinal holds Card b₁ c= b₁

proof

let c₁ be Ordinal;
E10: ex b₁ being Ordinal st
( Card c₁ = b₁ & for b₂ being Ordinal holds
( b₂,b₁ are_equipotent implies b₁ c= b₂ ) ) by E2;
c₁, Card c₁ are_equipotent by E5;
hence Card c₁ c= c₁ by E10;

end;

theorem :: CARD_1:25

for b₁ being set
for b₂ being Cardinal holds
( b₁ in b₂ implies Card b₁ <` b₂ )

proof

let c₁ be set ;
let c₂ be Cardinal;
assume E10: c₁ in c₂ ;
then reconsider c₃ = c₁ as Ordinal by ORDINAL1:23;
( Card c₃ c= c₃ & Card c₁ = Card c₃ ) by E9;
hence Card c₁ in c₂ by E10, ORDINAL1:22;

end;

theorem E10: :: CARD_1:26

for b₁, b₂ being set holds
( Card b₁ <=` Card b₂ iff ex b₃ being Function st
( b₃ is one-to-one & dom b₃ = b₁ & rng b₃ c= b₂ ) )

proof

let c₁, c₂ be set ;
thus not ( Card c₁ <=` Card c₂ & for b₁ being Function holds
not ( b₁ is one-to-one & dom b₁ = c₁ & rng b₁ c= c₂ ) )

proof

assume E11: Card c₁ c= Card c₂ ;
E12: ( c₁, Card c₁ are_equipotent & c₂, Card c₂ are_equipotent ) by E5;
then consider c₃ being Function such that
E13: ( c₃ is one-to-one & dom c₃ = c₁ & rng c₃ = Card c₁ ) by WELLORD2:def 4;
consider c₄ being Function such that
E14: ( c₄ is one-to-one & dom c₄ = c₂ & rng c₄ = Card c₂ ) by E12, WELLORD2:def 4;
take c₅ = c₃ * (c₄ " );
c₄ " is one-to-one by E14, FUNCT_1:62;
hence c₅ is one-to-one by E13, FUNCT_1:46;
( rng c₄ = dom (c₄ " ) & dom c₄ = rng (c₄ " ) ) by E14, FUNCT_1:55;
hence ( dom c₅ = c₁ & rng c₅ c= c₂ ) by E11, E13, E14, RELAT_1:45, RELAT_1:46;

end;

given c₃ being Function such that E11: ( c₃ is one-to-one & dom c₃ = c₁ & rng c₃ c= c₂ ) ;
c₂, Card c₂ are_equipotent by E5;
then consider c₄ being Function such that
E12: ( c₄ is one-to-one & dom c₄ = c₂ & rng c₄ = Card c₂ ) by WELLORD2:def 4;
E13: c₁, rng (c₃ * c₄) are_equipotent

proof

take c₃ * c₄ ; :: uses WELLORD2:def 4
thus c₃ * c₄ is one-to-one by E11, E12, FUNCT_1:46;
thus dom (c₃ * c₄) = c₁ by E11, E12, RELAT_1:46;
thus rng (c₃ * c₄) = rng (c₃ * c₄) ;

end;

rng (c₃ * c₄) c= Card c₂ by E12, RELAT_1:45;
then E14: Card (rng (c₃ * c₄)) <=` Card c₂ by E8;
( c₁, Card c₁ are_equipotent & rng (c₃ * c₄), Card (rng (c₃ * c₄)) are_equipotent ) by E5;
then ( Card c₁,c₁ are_equipotent & c₁, Card (rng (c₃ * c₄)) are_equipotent ) by E13, WELLORD2:22;
then Card c₁, Card (rng (c₃ * c₄)) are_equipotent by WELLORD2:22;
hence Card c₁ <=` Card c₂ by E14, E4;

end;

theorem E11: :: CARD_1:27

for b₁, b₂ being set holds
( b₁ c= b₂ implies Card b₁ <=` Card b₂ )

proof

let c₁, c₂ be set ;
assume E12: c₁ c= c₂ ;
ex b₁ being Function st
( b₁ is one-to-one & dom b₁ = c₁ & rng b₁ c= c₂ )

proof

take id c₁ ;
thus ( id c₁ is one-to-one & dom (id c₁) = c₁ & rng (id c₁) c= c₂ ) by E12, FUNCT_1:52, RELAT_1:71;

end;

hence Card c₁ <=` Card c₂ by E10;

end;

theorem :: CARD_1:28

for b₁, b₂ being set holds
( Card b₁ <=` Card b₂ iff ex b₃ being Function st
( dom b₃ = b₂ & b₁ c= rng b₃ ) )

proof

let c₁, c₂ be set ;
thus not ( Card c₁ <=` Card c₂ & for b₁ being Function holds
not ( dom b₁ = c₂ & c₁ c= rng b₁ ) )

proof

assume Card c₁ <=` Card c₂ ;
then consider c₃ being Function such that
E12: ( c₃ is one-to-one & dom c₃ = c₁ & rng c₃ c= c₂ ) by E10;
defpred S₁[ set , set ] means ( ( a₁ in rng c₃ & a₂ = (c₃ " ) . a₁ ) or ( not a₁ in rng c₃ & a₂ = 0 ) );
E13: for b₁ being set holds
not ( b₁ in c₂ & for b₂ being set holds
not S₁[b₁,b₂] )

proof

let c₄ be set ;
assume c₄ in c₂ ;
not ( not c₄ in rng c₃ & for b₁ being set holds
not S₁[c₄,b₁] ) ;
hence ex b₁ being set st
S₁[c₄,b₁] ;

end;

E14: for b₁, b₂, b₃ being set holds
( ( b₁ in c₂ & S₁[b₁,b₂] & S₁[b₁,b₃] ) implies ( b₂ = b₃ ) ) ;
consider c₄ being Function such that
E15: ( dom c₄ = c₂ & for b₁ being set holds
( b₁ in c₂ implies S₁[b₁,c₄ . b₁] ) ) from FUNCT_1:sch 2(E14, E13);
take c₄ ;
thus dom c₄ = c₂ by E15;
let c₅ be set ; :: uses TARSKI:def 3
assume c₅ in c₁ ;
then E16: ( (c₃ " ) . (c₃ . c₅) = c₅ & c₃ . c₅ in rng c₃ ) by E12, FUNCT_1:56, FUNCT_1:def 5;
then c₅ = c₄ . (c₃ . c₅) by E12, E15;
hence c₅ in rng c₄ by E12, E15, E16, FUNCT_1:def 5;

end;

given c₃ being Function such that E12: ( dom c₃ = c₂ & c₁ c= rng c₃ ) ;
deffunc H₁( set ) -> set = c₃ " {a₁};
consider c₄ being Function such that
E13: ( dom c₄ = c₁ & for b₁ being set holds
( b₁ in c₁ implies c₄ . b₁ = H₁(b₁) ) ) from FUNCT_1:sch 3();
E14: ( c₁ = {} implies Card c₁ <=` Card c₂ )

proof

assume c₁ = {} ;
then c₁ c= c₂ by XBOOLE_1:2;
hence Card c₁ <=` Card c₂ by E11;

end;

( c₁ <> {} implies Card c₁ <=` Card c₂ )

proof

assume c₁ <> {} ;
then reconsider c₅ = rng c₄ as non empty set by E13, RELAT_1:65;
for b₁ being set holds
not ( b₁ in c₅ & not b₁ <> {} )

proof

let c₆ be set ;
assume c₆ in c₅ ;
then consider c₇ being set such that
E15: ( c₇ in dom c₄ & c₆ = c₄ . c₇ ) by FUNCT_1:def 5;
E16: ( c₆ = c₃ " {c₇} & c₇ in rng c₃ ) by E12, E13, E15;
consider c₈ being set such that
E17: ( c₈ in dom c₃ & c₇ = c₃ . c₈ ) by E12, E13, E15, FUNCT_1:def 5;
c₇ in {c₇} by TARSKI:def 1;
hence c₆ <> {} by E16, E17, FUNCT_1:def 13;

end;

then consider c₆ being Function such that
E15: ( dom c₆ = c₅ & for b₁ being set holds
( b₁ in c₅ implies c₆ . b₁ in b₁ ) ) by WELLORD2:28;
E16: dom (c₄ * c₆) = c₁ by E13, E15, RELAT_1:46;
E17: c₄ * c₆ is one-to-one

proof

let c₇ be set ; :: uses FUNCT_1:def 8
let c₈ be set ;
assume E18: ( c₇ in dom (c₄ * c₆) & c₈ in dom (c₄ * c₆) & (c₄ * c₆) . c₇ = (c₄ * c₆) . c₈ ) ;
then E19: ( c₄ . c₇ = c₃ " {c₇} & c₄ . c₈ = c₃ " {c₈} & (c₄ * c₆) . c₇ = c₆ . (c₄ . c₇) & (c₄ * c₆) . c₈ = c₆ . (c₄ . c₈) ) by E13, E16, FUNCT_1:23;
then ( c₆ . (c₃ " {c₇}) = c₆ . (c₃ " {c₈}) & c₃ " {c₇} in c₅ & c₃ " {c₈} in c₅ ) by E13, E16, E18, FUNCT_1:def 5;
then ( c₆ . (c₃ " {c₇}) in c₃ " {c₇} & c₆ . (c₃ " {c₈}) in c₃ " {c₈} ) by E15;
then ( c₃ . (c₆ . (c₃ " {c₇})) in {c₇} & c₃ . (c₆ . (c₃ " {c₈})) in {c₈} ) by FUNCT_1:def 13;
then ( c₃ . (c₆ . (c₃ " {c₇})) = c₇ & c₃ . (c₆ . (c₃ " {c₈})) = c₈ ) by TARSKI:def 1;
hence c₇ = c₈ by E18, E19;

end;

rng (c₄ * c₆) c= c₂

proof

let c₇ be set ; :: uses TARSKI:def 3
assume c₇ in rng (c₄ * c₆) ;
then consider c₈ being set such that
E18: ( c₈ in dom (c₄ * c₆) & c₇ = (c₄ * c₆) . c₈ ) by FUNCT_1:def 5;
E19: ( c₄ . c₈ = c₃ " {c₈} & c₇ = c₆ . (c₄ . c₈) ) by E13, E16, E18, FUNCT_1:23;
then c₃ " {c₈} in c₅ by E13, E16, E18, FUNCT_1:def 5;
then c₇ in c₃ " {c₈} by E15, E19;
hence c₇ in c₂ by E12, FUNCT_1:def 13;

end;

hence Card c₁ <=` Card c₂ by E16, E17, E10;

end;

hence Card c₁ <=` Card c₂ by E14;

end;

theorem E12: :: CARD_1:29

for b₁ being set holds
not b₁, bool b₁ are_equipotent

proof

let c₁ be set ;
given c₂ being Function such that E13: ( c₂ is one-to-one & dom c₂ = c₁ & rng c₂ = bool c₁ ) ; :: uses WELLORD2:def 4
defpred S₁[ set ] means for b₁ being set holds
not ( b₁ = c₂ . a₁ & a₁ in b₁ );
consider c₃ being set such that
E14: for b₁ being set holds
( b₁ in c₃ iff ( b₁ in c₁ & S₁[b₁] ) ) from XBOOLE_0:sch 1();
c₃ c= c₁

proof

let c₄ be set ; :: uses TARSKI:def 3
thus not ( c₄ <` c₃ & not c₄ <` c₁ ) by E14;

end;

then consider c₄ being set such that
E15: ( c₄ in c₁ & c₃ = c₂ . c₄ ) by E13, FUNCT_1:def 5;
not c₄ in c₃ by E14, E15;
then ex b₁ being set st
( b₁ = c₂ . c₄ & c₄ in b₁ ) by E14, E15;
hence not verum by E14, E15;

end;

theorem E13: :: CARD_1:30

for b₁ being set holds Card b₁ <` Card (bool b₁)

proof

let c₁ be set ;
deffunc H₁( set ) -> set = {a₁};
consider c₂ being Function such that
E14: ( dom c₂ = c₁ & for b₁ being set holds
( b₁ in c₁ implies c₂ . b₁ = H₁(b₁) ) ) from FUNCT_1:sch 3();
E15: c₂ is one-to-one

proof

let c₃ be set ; :: uses FUNCT_1:def 8
let c₄ be set ;
assume E16: ( c₃ in dom c₂ & c₄ in dom c₂ & c₂ . c₃ = c₂ . c₄ ) ;
then ( c₂ . c₃ = {c₃} & c₂ . c₄ = {c₄} ) by E14;
hence c₃ = c₄ by E16, ZFMISC_1:6;

end;

rng c₂ c= bool c₁

proof

let c₃ be set ; :: uses TARSKI:def 3
assume c₃ in rng c₂ ;
then consider c₄ being set such that
E16: ( c₄ in dom c₂ & c₃ = c₂ . c₄ ) by FUNCT_1:def 5;
E17: c₂ . c₄ = {c₄} by E14, E16;
{c₄} c= c₁

proof

let c₅ be set ; :: uses TARSKI:def 3
assume c₅ in {c₄} ;
hence c₅ <` c₁ by E14, E16, TARSKI:def 1;

end;

hence c₃ <` bool c₁ by E16, E17;

end;

then E16: Card c₁ <=` Card (bool c₁) by E14, E15, E10;
not c₁, bool c₁ are_equipotent by E12;
then Card c₁ <> Card (bool c₁) by E6;
then Card c₁ c< Card (bool c₁) by E16, XBOOLE_0:def 8;
hence Card c₁ <` Card (bool c₁) by ORDINAL1:21;

end;

definition

let c₁ be set ;
func nextcard a₁ -> Cardinal means :E14: :: CARD_1:def 6
( Card a₁ <` a₂ & for b₁ being Cardinal holds
( Card a₁ <` b₁ implies a₂ <=` b₁ ) );
existence

proof

defpred S₁[ Ordinal] means ex b₁ being Cardinal st
( a₁ = b₁ & Card c₁ <` b₁ );
( Card c₁ <` Card (bool c₁) & Card (bool c₁) = Card (bool c₁) ) by E13;
then E14: ex b₁ being Ordinal st
S₁[b₁] ;
consider c₂ being Ordinal such that
E15: S₁[c₂]
and E16: for b₁ being Ordinal holds
( S₁[b₁] implies c₂ c= b₁ ) from ORDINAL1:sch 1(E14);
consider c₃ being Cardinal such that
E17: ( c₂ = c₃ & Card c₁ <` c₃ ) by E15;
take c₃ ;
thus Card c₁ <` c₃ by E17;
let c₄ be Cardinal;
assume Card c₁ <` c₄ ;
hence c₃ c= c₄ by E16, E17;

end;

uniqueness

proof

let c₂, c₃ be Cardinal;
assume that E14: ( Card c₁ <` c₂ & for b₁ being Cardinal holds
( Card c₁ <` b₁ implies c₂ <=` b₁ ) )
and E15: ( Card c₁ <` c₃ & for b₁ being Cardinal holds
( Card c₁ <` b₁ implies c₃ <=` b₁ ) ) ;
( c₂ <=` c₃ & c₃ <=` c₂ ) by E14, E15;
hence c₂ = c₃ by XBOOLE_0:def 10;

end;

:: deftheorem E14 defines nextcard CARD_1:def 6 :

theorem :: CARD_1:31

canceled;

theorem E15: :: CARD_1:32

for b₁ being Cardinal holds b₁ <` nextcard b₁

proof

let c₁ be Cardinal;
( Card c₁ <` nextcard c₁ & c₁ = Card c₁ ) by E5, E14;
hence c₁ <` nextcard c₁ ;

end;

theorem :: CARD_1:33

for b₁ being set holds Card {} <` nextcard b₁

proof

let c₁ be set ;
{} c= c₁ by XBOOLE_1:2;
then ( Card {} <=` Card c₁ & Card c₁ <` nextcard c₁ ) by E14, E11;
hence Card {} <` nextcard c₁ by ORDINAL1:22;

end;

theorem E16: :: CARD_1:34

for b₁, b₂ being set holds
( Card b₁ = Card b₂ implies nextcard b₁ = nextcard b₂ )

proof

let c₁, c₂ be set ;
assume E17: Card c₁ = Card c₂ ;
( Card c₁ <` nextcard c₁ & for b₁ being Cardinal holds
( Card c₁ <` b₁ implies nextcard c₁ <=` b₁ ) ) by E14;
hence nextcard c₁ = nextcard c₂ by E17, E14;

end;

theorem E17: :: CARD_1:35

for b₁, b₂ being set holds
( b₁,b₂ are_equipotent implies nextcard b₁ = nextcard b₂ )

proof

let c₁, c₂ be set ;
assume c₁,c₂ are_equipotent ;
then Card c₁ = Card c₂ by E6;
hence nextcard c₁ = nextcard c₂ by E16;

end;

theorem :: CARD_1:36

for b₁ being Ordinal holds b₁ in nextcard b₁

proof

let c₁ be Ordinal;
assume not c₁ in nextcard c₁ ;
then ( nextcard c₁ c= c₁ & c₁, Card c₁ are_equipotent ) by E5, ORDINAL1:26;
then ( Card (nextcard c₁) <=` Card c₁ & Card (nextcard c₁) = nextcard c₁ & nextcard (Card c₁) = nextcard c₁ & Card c₁ <` nextcard (Card c₁) ) by E5, E11, E15, E17;
hence not verum by ORDINAL1:7;

end;

definition

let c₁ be Cardinal;
attr a₁ is limit means :E18: :: CARD_1:def 7
for b₁ being Cardinal holds
not a₁ = nextcard b₁;

end;

:: deftheorem E18 defines limit CARD_1:def 7 :

notation

let c₁ be Cardinal;

end;

definition

let c₁ be Ordinal;
func alef a₁ -> set means :E19: :: CARD_1:def 8
ex b₁ being T-Sequence st
( a₂ = last b₁ & dom b₁ = succ a₁ & b₁ . {} = Card NAT & for b₂ being Ordinal holds
( succ b₂ in succ a₁ implies b₁ . (succ b₂) = nextcard (union {(b₁ . b₂)}) ) & for b₂ being Ordinal holds
( ( b₂ in succ a₁ & b₂ is is_limit_ordinal ) implies ( not b₂ <> {} or b₁ . b₂ = Card (sup (b₁ | b₂)) ) ) );
correctness

proof

deffunc H₁( Ordinal, set ) -> Cardinal = nextcard (union {a₂});
deffunc H₂( Ordinal, T-Sequence) -> Cardinal = Card (sup a₂);
set c₂ = Card NAT ;
thus ( ex b₁ being set ex b₂ being T-Sequence st
( b₁ = last b₂ & dom b₂ = succ c₁ & b₂ . {} = Card NAT & for b₃ being Ordinal holds
( succ b₃ in succ c₁ implies b₂ . (succ b₃) = H₁(b₃,b₂ . b₃) ) & for b₃ being Ordinal holds
( ( b₃ in succ c₁ & b₃ is is_limit_ordinal ) implies ( not b₃ <> {} or b₂ . b₃ = H₂(b₃,b₂ | b₃) ) ) ) & for b₁, b₂ being set holds
( ( ) implies ( for b₃ being T-Sequence holds
not ( b₁ = last b₃ & dom b₃ = succ c₁ & b₃ . {} = Card NAT & for b₄ being Ordinal holds
( succ b₄ in succ c₁ implies b₃ . (succ b₄) = H₁(b₄,b₃ . b₄) ) & for b₄ being Ordinal holds
( ( b₄ in succ c₁ & b₄ is is_limit_ordinal ) implies ( not b₄ <> {} or b₃ . b₄ = H₂(b₄,b₃ | b₄) ) ) ) or for b₃ being T-Sequence holds
not ( b₂ = last b₃ & dom b₃ = succ c₁ & b₃ . {} = Card NAT & for b₄ being Ordinal holds
( succ b₄ in succ c₁ implies b₃ . (succ b₄) = H₁(b₄,b₃ . b₄) ) & for b₄ being Ordinal holds
( ( b₄ in succ c₁ & b₄ is is_limit_ordinal ) implies ( not b₄ <> {} or b₃ . b₄ = H₂(b₄,b₃ | b₄) ) ) ) or b₁ = b₂ ) ) ) from ORDINAL2:sch 7();

end;

:: deftheorem E19 defines alef CARD_1:def 8 :

E20: now

deffunc H₁( Ordinal) -> set = alef a₁;
deffunc H₂( Ordinal, set ) -> Cardinal = nextcard (union {a₂});
deffunc H₃( Ordinal, T-Sequence) -> Cardinal = Card (sup a₂);
E21: for b₁ being Ordinal
for b₂ being set holds
( b₂ = H₁(b₁) iff ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = Card NAT & for b₄ being Ordinal holds
( succ b₄ in succ b₁ implies b₃ . (succ b₄) = H₂(b₄,b₃ . b₄) ) & for b₄ being Ordinal holds
( ( b₄ in succ b₁ & b₄ is is_limit_ordinal ) implies ( not b₄ <> {} or b₃ . b₄ = H₃(b₄,b₃ | b₄) ) ) ) ) by E19;
H₁( {} ) = Card NAT from ORDINAL2:sch 8(E21);
hence alef 0 = Card NAT ;
thus for b₁ being Ordinal holds H₁( succ b₁) = H₂(b₁,H₁(b₁)) from ORDINAL2:sch 9(E21);
thus for b₁ being Ordinal holds
( ( b₁ is is_limit_ordinal ) implies ( not b₁ <> {} or for b₂ being T-Sequence holds
( ( dom b₂ = b₁ & for b₃ being Ordinal holds
( b₃ in b₁ implies b₂ . b₃ = alef b₃ ) ) implies ( alef b₁ = Card (sup b₂) ) ) ) )

proof

let c₁ be Ordinal;
assume E22: ( c₁ <> {} & c₁ is is_limit_ordinal ) ;
let c₂ be T-Sequence;
assume that E23: dom c₂ = c₁
and E24: for b₁ being Ordinal holds
( b₁ in c₁ implies c₂ . b₁ = H₁(b₁) ) ;
thus H₁(c₁) = H₃(c₁,c₂) from ORDINAL2:sch 10(E21, E22, E23, E24);

end;

deffunc H₁( Ordinal) -> set = alef a₁;

registration

let c₁ be Ordinal;
cluster alef a₁ -> ordinal cardinal ;
coherence

proof

E21: now

given c₂ being Ordinal such that E22: c₁ = succ c₂ ;
alef c₁ = nextcard (union {(alef c₂)}) by E22, E20;
hence alef c₁ is cardinal ;

end;

now

assume E22: ( c₁ <> {} & for b₁ being Ordinal holds
c₁ <> succ b₁ ) ;
then E23: c₁ is is_limit_ordinal by ORDINAL1:42;
consider c₂ being T-Sequence such that
E24: ( dom c₂ = c₁ & for b₁ being Ordinal holds
( b₁ in c₁ implies c₂ . b₁ = H₁(b₁) ) ) from ORDINAL2:sch 2();
alef c₁ = Card (sup c₂) by E22, E23, E24, E20;
hence alef c₁ is Cardinal ;

end;

hence alef c₁ is cardinal by E21, E20;

end;

theorem :: CARD_1:37

canceled;

theorem :: CARD_1:38

alef 0 = Card NAT by E20;

theorem E21: :: CARD_1:39

for b₁ being Ordinal holds alef (succ b₁) = nextcard (alef b₁)

proof

let c₁ be Ordinal;
thus alef (succ c₁) = nextcard (union {(alef c₁)}) by E20
.= nextcard (alef c₁) by ZFMISC_1:31 ;

end;

theorem :: CARD_1:40

for b₁ being Ordinal holds
( ( b₁ is is_limit_ordinal ) implies ( not b₁ <> {} or for b₂ being T-Sequence holds
( ( dom b₂ = b₁ & for b₃ being Ordinal holds
( b₃ in b₁ implies b₂ . b₃ = alef b₃ ) ) implies ( alef b₁ = Card (sup b₂) ) ) ) ) by E20;

theorem E22: :: CARD_1:41

for b₁, b₂ being Ordinal holds
( b₁ in b₂ iff alef b₁ <` alef b₂ )

proof

let c₁, c₂ be Ordinal;
defpred S₁[ Ordinal] means for b₁ being Ordinal holds
( b₁ in a₁ implies alef b₁ <` alef a₁ );
E23: S₁[ {} ] ;
E24: for b₁ being Ordinal holds
( S₁[b₁] implies S₁[ succ b₁] )

proof

let c₃ be Ordinal;
assume E25: S₁[c₃] ;
let c₄ be Ordinal;
assume E26: c₄ in succ c₃ ;
E27: alef (succ c₃) = nextcard (alef c₃) by E21;
E28: ( c₄ c< c₃ iff ( c₄ c= c₃ & c₄ <> c₃ ) ) by XBOOLE_0:def 8;

now

assume c₄ in c₃ ;
then ( alef c₄ <` alef c₃ & alef c₃ <` nextcard (alef c₃) ) by E25, E15;
hence alef c₄ <` alef (succ c₃) by E27, ORDINAL1:19;

end;

hence alef c₄ <` alef (succ c₃) by E26, E27, E28, E15, ORDINAL1:21, ORDINAL1:34;

end;

E25: for b₁ being Ordinal holds
( ( b₁ is is_limit_ordinal & for b₂ being Ordinal holds
( b₂ in b₁ implies S₁[b₂] ) ) implies ( not b₁ <> {} or S₁[b₁] ) )

proof

let c₃ be Ordinal;
assume that E26: ( c₃ <> {} & c₃ is is_limit_ordinal )
and for b₁ being Ordinal holds
( b₁ in c₃ implies for b₂ being Ordinal holds
( b₂ in b₁ implies alef b₂ <` alef b₁ ) ) ;
consider c₄ being T-Sequence such that
E27: dom c₄ = c₃
and E28: for b₁ being Ordinal holds
( b₁ in c₃ implies c₄ . b₁ = H₁(b₁) ) from ORDINAL2:sch 2();
E29: alef c₃ = Card (sup c₄) by E26, E27, E28, E20;
let c₅ be Ordinal;
assume c₅ in c₃ ;
then succ c_5</