:: CARD_1 semantic presentation

Lemma1: for b1, b2 being Ordinal holds
( b1 c= b2 implies succ b1 c= succ b2 )
proof
let c1, c2 be Ordinal;
assume E2: c1 c= c2 ;
let c3 be set ; :: according to TARSKI:def 3
assume c3 in succ c1 ;
then E3: ( c3 in c1 or c3 = c1 ) by ORDINAL1:13;
c2 in succ c2 by ORDINAL1:10;
then ( ( c3 in c2 or c3 in succ c2 ) & c2 c= succ c2 ) by E2, E3, ORDINAL1:22;
hence c3 <` succ c2 ;
end;

definition
let c1 be set ;
attr a1 is cardinal means :Def1: :: CARD_1:def 1
ex b1 being Ordinal st
( a1 = b1 & ( for b2 being Ordinal holds
( b2,b1 are_equipotent implies b1 c= b2 ) ) );
end;

:: deftheorem Def1 defines cardinal CARD_1:def 1 :
for b1 being set holds
( b1 is cardinal iff ex b2 being Ordinal st
( b1 = b2 & ( for b3 being Ordinal holds
( b3,b2 are_equipotent implies b2 c= b3 ) ) ) );

registration
cluster cardinal set ;
existence
ex b1 being set st b1 is cardinal
proof
consider c1 being Ordinal;
defpred S1[ Ordinal] means a1,c1 are_equipotent ;
E3: ex b1 being Ordinal st
S1[b1] ;
consider c2 being Ordinal such that
E4: ( S1[c2] & ( for b1 being Ordinal holds
( S1[b1] implies c2 c= b1 ) ) ) from ORDINAL1:sch 1(E3);
 reconsider c3 = c2 as set ;
take c3 ;
take c2 ; :: according to CARD_1:def 1
thus c3 = c2 ;
let c4 be Ordinal;
assume c4,c2 are_equipotent ;
then c4,c1 are_equipotent by E4, WELLORD2:22;
hence c2 c= c4 by E4;
end;
end;

definition
mode Cardinal is cardinal set ;
end;

registration
cluster cardinal -> ordinal set ;
coherence
for b1 being set holds
( b1 is cardinal implies b1 is ordinal )
proof
let c1 be set ;
assume c1 is cardinal ;
then ex b1 being Ordinal st
( c1 = b1 & ( for b2 being Ordinal holds
( b2,b1 are_equipotent implies b1 c= b2 ) ) ) by Def1;
hence c1 is ordinal ;
end;
end;

theorem Th1: :: CARD_1:1
canceled;

theorem Th2: :: CARD_1:2
canceled;

theorem Th3: :: CARD_1:3
canceled;

theorem Th4: :: CARD_1:4
for b1 being set holds
ex b2 being Ordinal st b1,b2 are_equipotent
proof
let c1 be set ;
consider c2 being Relation such that
E4: c2 well_orders c1 by WELLORD2:26;
set c3 = c2 |_2 c1;
E5: ( field (c2 |_2 c1) = c1 & c2 |_2 c1 is well-ordering ) by E4, WELLORD2:25;
take c4 = order_type_of (c2 |_2 c1);
c2 |_2 c1, RelIncl c4 are_isomorphic by E5, WELLORD2:def 2;
then consider c5 being Function such that
E6: c5 is_isomorphism_of c2 |_2 c1, RelIncl c4 by WELLORD1:def 8;
E7: ( dom c5 = field (c2 |_2 c1) & rng c5 = field (RelIncl c4) & c5 is one-to-one & ( for b1, b2 being set holds
( [b1,b2] in c2 |_2 c1 iff ( b1 in field (c2 |_2 c1) & b2 in field (c2 |_2 c1) & [(c5 . b1),(c5 . b2)] in RelIncl c4 ) ) ) ) by E6, WELLORD1:def 7;
take c5 ; :: according to WELLORD2:def 4
thus ( c5 is one-to-one & dom c5 = c1 & rng c5 = c4 ) by E4, E7, WELLORD2:25, WELLORD2:def 1;
end;

notation
let c1, c2 be Cardinal;
synonym c1 <=` c2 for c1 c= c2;
synonym c1 <` c2 for c1 in c2;
end;

theorem Th5: :: CARD_1:5
canceled;

theorem Th6: :: CARD_1:6
canceled;

theorem Th7: :: CARD_1:7
canceled;

theorem Th8: :: CARD_1:8
for b1, b2 being Cardinal holds
( b1 = b2 iff b1,b2 are_equipotent )
proof
let c1, c2 be Cardinal;
thus ( c1 = c2 implies c1,c2 are_equipotent ) ;
consider c3 being Ordinal such that
E5: ( c1 = c3 & ( for b1 being Ordinal holds
( b1,c3 are_equipotent implies c3 c= b1 ) ) ) by Def1;
consider c4 being Ordinal such that
E6: ( c2 = c4 & ( for b1 being Ordinal holds
( b1,c4 are_equipotent implies c4 c= b1 ) ) ) by Def1;
assume E7: c1,c2 are_equipotent ;
then E8: ( c4 c= c3 & c2,c1 are_equipotent ) by E5, E6;
c3 c= c4 by E5, E6, E7;
hence c1 = c2 by E5, E6, E8, XBOOLE_0:def 10;
end;

theorem Th9: :: CARD_1:9
canceled;

theorem Th10: :: CARD_1:10
canceled;

theorem Th11: :: CARD_1:11
canceled;

theorem Th12: :: CARD_1:12
canceled;

theorem Th13: :: CARD_1:13
for b1, b2 being Cardinal holds
( b1 <` b2 iff ( b1 <=` b2 & b1 <> b2 ) )
proof
let c1, c2 be Cardinal;
( c1 c< c2 iff ( c1 c= c2 & c1 <> c2 ) ) by XBOOLE_0:def 8;
hence ( c1 <` c2 iff ( c1 <=` c2 & c1 <> c2 ) ) by ORDINAL1:21, ORDINAL1:def 2;
end;

theorem Th14: :: CARD_1:14
for b1, b2 being Cardinal holds
( b1 <` b2 iff not b2 <=` b1 ) by ORDINAL1:7, ORDINAL1:26;

definition
let c1 be set ;
canceled;
canceled;
canceled;
func Card c1 -> Cardinal means :Def5: :: CARD_1:def 5
a1,a2 are_equipotent ;
existence
ex b1 being Cardinal st c1,b1 are_equipotent
proof
defpred S1[ Ordinal] means a1,c1 are_equipotent ;
E5: ex b1 being Ordinal st
S1[b1] by Th4;
consider c2 being Ordinal such that
E6: ( S1[c2] & ( for b1 being Ordinal holds
( S1[b1] implies c2 c= b1 ) ) ) from ORDINAL1:sch 1(E5);
 c2 is cardinal
proof
take c2 ; :: according to CARD_1:def 1
thus c2 = c2 ;
let c3 be Ordinal;
assume c3,c2 are_equipotent ;
then c1,c3 are_equipotent by E6, WELLORD2:22;
hence c2 c= c3 by E6;
end;
then reconsider c3 = c2 as Cardinal ;
take c3 ;
thus c1,c3 are_equipotent by E6;
end;
uniqueness
for b1, b2 being Cardinal holds
( c1,b1 are_equipotent & c1,b2 are_equipotent implies b1 = b2 )
proof
let c2, c3 be Cardinal;
assume that
E5: c1,c2 are_equipotent and
E6: c1,c3 are_equipotent ;
c2,c3 are_equipotent by E5, E6, WELLORD2:22;
hence c2 = c3 by Th8;
end;
end;

:: deftheorem Def2 CARD_1:def 2 :
canceled;

:: deftheorem Def3 CARD_1:def 3 :
canceled;

:: deftheorem Def4 CARD_1:def 4 :
canceled;

:: deftheorem Def5 defines Card CARD_1:def 5 :
for b1 being set
for b2 being Cardinal holds
( b2 = Card b1 iff b1,b2 are_equipotent );

theorem Th15: :: CARD_1:15
canceled;

theorem Th16: :: CARD_1:16
canceled;

theorem Th17: :: CARD_1:17
canceled;

theorem Th18: :: CARD_1:18
canceled;

theorem Th19: :: CARD_1:19
canceled;

theorem Th20: :: CARD_1:20
canceled;

theorem Th21: :: CARD_1:21
for b1, b2 being set holds
( b1,b2 are_equipotent iff Card b1 = Card b2 )
proof
let c1, c2 be set ;
E7: ( c1, Card c1 are_equipotent & c2, Card c2 are_equipotent ) by Def5;
thus ( c1,c2 are_equipotent implies Card c1 = Card c2 )
proof
assume c1,c2 are_equipotent ;
then Card c1,c2 are_equipotent by E7, WELLORD2:22;
hence Card c1 = Card c2 by Def5;
end;
assume Card c1 = Card c2 ;
hence c1,c2 are_equipotent by E7, WELLORD2:22;
end;

theorem Th22: :: CARD_1:22
for b1 being Relation holds
( b1 is well-ordering implies field b1, order_type_of b1 are_equipotent )
proof
let c1 be Relation;
assume c1 is well-ordering ;
then c1, RelIncl (order_type_of c1) are_isomorphic by WELLORD2:def 2;
then consider c2 being Function such that
E8: c2 is_isomorphism_of c1, RelIncl (order_type_of c1) by WELLORD1:def 8;
take c2 ; :: according to WELLORD2:def 4
field (RelIncl (order_type_of c1)) = order_type_of c1 by WELLORD2:def 1;
hence ( c2 is one-to-one & dom c2 = field c1 & rng c2 = order_type_of c1 ) by E8, WELLORD1:def 7;
end;

theorem Th23: :: CARD_1:23
for b1 being set
for b2 being Cardinal holds
( b1 c= b2 implies Card b1 <=` b2 )
proof
let c1 be set ;
let c2 be Cardinal;
defpred S1[ Ordinal] means ( a1 c= c2 & c1,a1 are_equipotent );
reconsider c3 = c2 as Ordinal ;
assume c1 c= c2 ;
then E9: ( order_type_of (RelIncl c1) c= c3 & RelIncl c1 is well-ordering & field (RelIncl c1) = c1 ) by WELLORD2:9, WELLORD2:17, WELLORD2:def 1;
then c1, order_type_of (RelIncl c1) are_equipotent by Th22;
then E10: ex b1 being Ordinal st
S1[b1] by E9;
consider c4 being Ordinal such that
E11: ( S1[c4] & ( for b1 being Ordinal holds
( S1[b1] implies c4 c= b1 ) ) ) from ORDINAL1:sch 1(E10);
 c4 is cardinal
proof
take c4 ; :: according to CARD_1:def 1
thus c4 = c4 ;
let c5 be Ordinal;
assume c5,c4 are_equipotent ;
then E12: c1,c5 are_equipotent by E11, WELLORD2:22;
assume E13: not c4 c= c5 ;
then c3 c= c5 by E11, E12;
hence not verum by E11, E13, XBOOLE_1:1;
end;
then reconsider c5 = c4 as Cardinal ;
Card c1 = c5 by E11, Def5;
hence Card c1 c= c2 by E11;
end;

theorem Th24: :: CARD_1:24
for b1 being Ordinal holds Card b1 c= b1
proof
let c1 be Ordinal;
E10: ex b1 being Ordinal st
( Card c1 = b1 & ( for b2 being Ordinal holds
( b2,b1 are_equipotent implies b1 c= b2 ) ) ) by Def1;
c1, Card c1 are_equipotent by Def5;
hence Card c1 c= c1 by E10;
end;

theorem Th25: :: CARD_1:25
for b1 being set
for b2 being Cardinal holds
( b1 in b2 implies Card b1 <` b2 )
proof
let c1 be set ;
let c2 be Cardinal;
assume E10: c1 in c2 ;
then reconsider c3 = c1 as Ordinal by ORDINAL1:23;
( Card c3 c= c3 & Card c1 = Card c3 ) by Th24;
hence Card c1 in c2 by E10, ORDINAL1:22;
end;

theorem Th26: :: CARD_1:26
for b1, b2 being set holds
( Card b1 <=` Card b2 iff ex b3 being Function st
( b3 is one-to-one & dom b3 = b1 & rng b3 c= b2 ) )
proof
let c1, c2 be set ;
thus not ( Card c1 <=` Card c2 & ( for b1 being Function holds
not ( b1 is one-to-one & dom b1 = c1 & rng b1 c= c2 ) ) )
proof
assume E11: Card c1 c= Card c2 ;
E12: ( c1, Card c1 are_equipotent & c2, Card c2 are_equipotent ) by Def5;
then consider c3 being Function such that
E13: ( c3 is one-to-one & dom c3 = c1 & rng c3 = Card c1 ) by WELLORD2:def 4;
consider c4 being Function such that
E14: ( c4 is one-to-one & dom c4 = c2 & rng c4 = Card c2 ) by E12, WELLORD2:def 4;
take c5 = (c4 " ) * c3;
c4 " is one-to-one by E14, FUNCT_1:62;
hence c5 is one-to-one by E13, FUNCT_1:46;
( rng c4 = dom (c4 " ) & dom c4 = rng (c4 " ) ) by E14, FUNCT_1:55;
hence ( dom c5 = c1 & rng c5 c= c2 ) by E11, E13, E14, RELAT_1:45, RELAT_1:46;
end;
given c3 being Function such that E11: ( c3 is one-to-one & dom c3 = c1 & rng c3 c= c2 ) ;
c2, Card c2 are_equipotent by Def5;
then consider c4 being Function such that
E12: ( c4 is one-to-one & dom c4 = c2 & rng c4 = Card c2 ) by WELLORD2:def 4;
E13: c1, rng (c4 * c3) are_equipotent
proof
take c4 * c3 ; :: according to WELLORD2:def 4
thus c4 * c3 is one-to-one by E11, E12, FUNCT_1:46;
thus dom (c4 * c3) = c1 by E11, E12, RELAT_1:46;
thus rng (c4 * c3) = rng (c4 * c3) ;
end;
rng (c4 * c3) c= Card c2 by E12, RELAT_1:45;
then E14: Card (rng (c4 * c3)) <=` Card c2 by Th23;
( c1, Card c1 are_equipotent & rng (c4 * c3), Card (rng (c4 * c3)) are_equipotent ) by Def5;
then ( Card c1,c1 are_equipotent & c1, Card (rng (c4 * c3)) are_equipotent ) by E13, WELLORD2:22;
then Card c1, Card (rng (c4 * c3)) are_equipotent by WELLORD2:22;
hence Card c1 <=` Card c2 by E14, Th8;
end;

theorem Th27: :: CARD_1:27
for b1, b2 being set holds
( b1 c= b2 implies Card b1 <=` Card b2 )
proof
let c1, c2 be set ;
assume E12: c1 c= c2 ;
ex b1 being Function st
( b1 is one-to-one & dom b1 = c1 & rng b1 c= c2 )
proof
take id c1 ;
thus ( id c1 is one-to-one & dom (id c1) = c1 & rng (id c1) c= c2 ) by E12, FUNCT_1:52, RELAT_1:71;
end;
hence Card c1 <=` Card c2 by Th26;
end;

theorem Th28: :: CARD_1:28
for b1, b2 being set holds
( Card b1 <=` Card b2 iff ex b3 being Function st
( dom b3 = b2 & b1 c= rng b3 ) )
proof
let c1, c2 be set ;
thus not ( Card c1 <=` Card c2 & ( for b1 being Function holds
not ( dom b1 = c2 & c1 c= rng b1 ) ) )
proof
assume Card c1 <=` Card c2 ;
then consider c3 being Function such that
E12: ( c3 is one-to-one & dom c3 = c1 & rng c3 c= c2 ) by Th26;
defpred S1[ set , set ] means ( ( a1 in rng c3 & a2 = (c3 " ) . a1 ) or ( not a1 in rng c3 & a2 = 0 ) );
E13: for b1 being set holds
not ( b1 in c2 & ( for b2 being set holds
not S1[b1,b2] ) )
proof
let c4 be set ;
assume c4 in c2 ;
not ( not c4 in rng c3 & ( for b1 being set holds
not S1[c4,b1] ) ) ;
hence ex b1 being set st
S1[c4,b1] ;
end;
E14: for b1, b2, b3 being set holds
( b1 in c2 & S1[b1,b2] & S1[b1,b3] implies b2 = b3 ) ;
consider c4 being Function such that
E15: ( dom c4 = c2 & ( for b1 being set holds
( b1 in c2 implies S1[b1,c4 . b1] ) ) ) from FUNCT_1:sch 2(E14, E13);
 take c4 ;
thus dom c4 = c2 by E15;
let c5 be set ; :: according to TARSKI:def 3
assume c5 in c1 ;
then E16: ( (c3 " ) . (c3 . c5) = c5 & c3 . c5 in rng c3 ) by E12, FUNCT_1:56, FUNCT_1:def 5;
then c5 = c4 . (c3 . c5) by E12, E15;
hence c5 in rng c4 by E12, E15, E16, FUNCT_1:def 5;
end;
given c3 being Function such that E12: ( dom c3 = c2 & c1 c= rng c3 ) ;
deffunc H1( set ) -> set = c3 " {a1};
consider c4 being Function such that
E13: ( dom c4 = c1 & ( for b1 being set holds
( b1 in c1 implies c4 . b1 = H1(b1) ) ) ) from FUNCT_1:sch 3();
 E14: ( c1 = {} implies Card c1 <=` Card c2 )
proof
assume c1 = {} ;
then c1 c= c2 by XBOOLE_1:2;
hence Card c1 <=` Card c2 by Th27;
end;
( c1 <> {} implies Card c1 <=` Card c2 )
proof
assume c1 <> {} ;
then reconsider c5 = rng c4 as non empty set by E13, RELAT_1:65;
for b1 being set holds
not ( b1 in c5 & not b1 <> {} )
proof
let c6 be set ;
assume c6 in c5 ;
then consider c7 being set such that
E15: ( c7 in dom c4 & c6 = c4 . c7 ) by FUNCT_1:def 5;
E16: ( c6 = c3 " {c7} & c7 in rng c3 ) by E12, E13, E15;
consider c8 being set such that
E17: ( c8 in dom c3 & c7 = c3 . c8 ) by E12, E13, E15, FUNCT_1:def 5;
c7 in {c7} by TARSKI:def 1;
hence c6 <> {} by E16, E17, FUNCT_1:def 13;
end;
then consider c6 being Function such that
E15: ( dom c6 = c5 & ( for b1 being set holds
( b1 in c5 implies c6 . b1 in b1 ) ) ) by WELLORD2:28;
E16: dom (c6 * c4) = c1 by E13, E15, RELAT_1:46;
E17: c6 * c4 is one-to-one
proof
let c7 be set ; :: according to FUNCT_1:def 8
let c8 be set ;
assume E18: ( c7 in dom (c6 * c4) & c8 in dom (c6 * c4) & (c6 * c4) . c7 = (c6 * c4) . c8 ) ;
then E19: ( c4 . c7 = c3 " {c7} & c4 . c8 = c3 " {c8} & (c6 * c4) . c7 = c6 . (c4 . c7) & (c6 * c4) . c8 = c6 . (c4 . c8) ) by E13, E16, FUNCT_1:23;
then ( c6 . (c3 " {c7}) = c6 . (c3 " {c8}) & c3 " {c7} in c5 & c3 " {c8} in c5 ) by E13, E16, E18, FUNCT_1:def 5;
then ( c6 . (c3 " {c7}) in c3 " {c7} & c6 . (c3 " {c8}) in c3 " {c8} ) by E15;
then ( c3 . (c6 . (c3 " {c7})) in {c7} & c3 . (c6 . (c3 " {c8})) in {c8} ) by FUNCT_1:def 13;
then ( c3 . (c6 . (c3 " {c7})) = c7 & c3 . (c6 . (c3 " {c8})) = c8 ) by TARSKI:def 1;
hence c7 = c8 by E18, E19;
end;
rng (c6 * c4) c= c2
proof
let c7 be set ; :: according to TARSKI:def 3
assume c7 in rng (c6 * c4) ;
then consider c8 being set such that
E18: ( c8 in dom (c6 * c4) & c7 = (c6 * c4) . c8 ) by FUNCT_1:def 5;
E19: ( c4 . c8 = c3 " {c8} & c7 = c6 . (c4 . c8) ) by E13, E16, E18, FUNCT_1:23;
then c3 " {c8} in c5 by E13, E16, E18, FUNCT_1:def 5;
then c7 in c3 " {c8} by E15, E19;
hence c7 in c2 by E12, FUNCT_1:def 13;
end;
hence Card c1 <=` Card c2 by E16, E17, Th26;
end;
hence Card c1 <=` Card c2 by E14;
end;

theorem Th29: :: CARD_1:29
for b1 being set holds
not b1, bool b1 are_equipotent
proof
let c1 be set ;
given c2 being Function such that E13: ( c2 is one-to-one & dom c2 = c1 & rng c2 = bool c1 ) ; :: according to WELLORD2:def 4
defpred S1[ set ] means for b1 being set holds
not ( b1 = c2 . a1 & a1 in b1 );
consider c3 being set such that
E14: for b1 being set holds
( b1 in c3 iff ( b1 in c1 & S1[b1] ) ) from XBOOLE_0:sch 1();
 c3 c= c1
proof
let c4 be set ; :: according to TARSKI:def 3
thus not ( c4 <` c3 & not c4 <` c1 ) by E14;
end;
then consider c4 being set such that
E15: ( c4 in c1 & c3 = c2 . c4 ) by E13, FUNCT_1:def 5;
not c4 in c3 by E14, E15;
then ex b1 being set st
( b1 = c2 . c4 & c4 in b1 ) by E14, E15;
hence not verum by E14, E15;
end;

theorem Th30: :: CARD_1:30
for b1 being set holds Card b1 <` Card (bool b1)
proof
let c1 be set ;
deffunc H1( set ) -> set = {a1};
consider c2 being Function such that
E14: ( dom c2 = c1 & ( for b1 being set holds
( b1 in c1 implies c2 . b1 = H1(b1) ) ) ) from FUNCT_1:sch 3();
 E15: c2 is one-to-one
proof
let c3 be set ; :: according to FUNCT_1:def 8
let c4 be set ;
assume E16: ( c3 in dom c2 & c4 in dom c2 & c2 . c3 = c2 . c4 ) ;
then ( c2 . c3 = {c3} & c2 . c4 = {c4} ) by E14;
hence c3 = c4 by E16, ZFMISC_1:6;
end;
rng c2 c= bool c1
proof
let c3 be set ; :: according to TARSKI:def 3
assume c3 in rng c2 ;
then consider c4 being set such that
E16: ( c4 in dom c2 & c3 = c2 . c4 ) by FUNCT_1:def 5;
E17: c2 . c4 = {c4} by E14, E16;
{c4} c= c1
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in {c4} ;
hence c5 <` c1 by E14, E16, TARSKI:def 1;
end;
hence c3 <` bool c1 by E16, E17;
end;
then E16: Card c1 <=` Card (bool c1) by E14, E15, Th26;
not c1, bool c1 are_equipotent by Th29;
then Card c1 <> Card (bool c1) by Th21;
then Card c1 c< Card (bool c1) by E16, XBOOLE_0:def 8;
hence Card c1 <` Card (bool c1) by ORDINAL1:21;
end;

definition
let c1 be set ;
func nextcard c1 -> Cardinal means :Def6: :: CARD_1:def 6
( Card a1 <` a2 & ( for b1 being Cardinal holds
( Card a1 <` b1 implies a2 <=` b1 ) ) );
existence
ex b1 being Cardinal st
( Card c1 <` b1 & ( for b2 being Cardinal holds
( Card c1 <` b2 implies b1 <=` b2 ) ) )
proof
defpred S1[ Ordinal] means ex b1 being Cardinal st
( a1 = b1 & Card c1 <` b1 );
( Card c1 <` Card (bool c1) & Card (bool c1) = Card (bool c1) ) by Th30;
then E14: ex b1 being Ordinal st
S1[b1] ;
consider c2 being Ordinal such that
E15: S1[c2] and
E16: for b1 being Ordinal holds
( S1[b1] implies c2 c= b1 ) from ORDINAL1:sch 1(E14);
 consider c3 being Cardinal such that
E17: ( c2 = c3 & Card c1 <` c3 ) by E15;
take c3 ;
thus Card c1 <` c3 by E17;
let c4 be Cardinal;
assume Card c1 <` c4 ;
hence c3 c= c4 by E16, E17;
end;
uniqueness
for b1, b2 being Cardinal holds
( Card c1 <` b1 & ( for b3 being Cardinal holds
( Card c1 <` b3 implies b1 <=` b3 ) ) & Card c1 <` b2 & ( for b3 being Cardinal holds
( Card c1 <` b3 implies b2 <=` b3 ) ) implies b1 = b2 )
proof
let c2, c3 be Cardinal;
assume that
E14: ( Card c1 <` c2 & ( for b1 being Cardinal holds
( Card c1 <` b1 implies c2 <=` b1 ) ) ) and
E15: ( Card c1 <` c3 & ( for b1 being Cardinal holds
( Card c1 <` b1 implies c3 <=` b1 ) ) ) ;
( c2 <=` c3 & c3 <=` c2 ) by E14, E15;
hence c2 = c3 by XBOOLE_0:def 10;
end;
end;

:: deftheorem Def6 defines nextcard CARD_1:def 6 :
for b1 being set
for b2 being Cardinal holds
( b2 = nextcard b1 iff ( Card b1 <` b2 & ( for b3 being Cardinal holds
( Card b1 <` b3 implies b2 <=` b3 ) ) ) );

theorem Th31: :: CARD_1:31
canceled;

theorem Th32: :: CARD_1:32
for b1 being Cardinal holds b1 <` nextcard b1
proof
let c1 be Cardinal;
( Card c1 <` nextcard c1 & c1 = Card c1 ) by Def5, Def6;
hence c1 <` nextcard c1 ;
end;

theorem Th33: :: CARD_1:33
for b1 being set holds Card {} <` nextcard b1
proof
let c1 be set ;
{} c= c1 by XBOOLE_1:2;
then ( Card {} <=` Card c1 & Card c1 <` nextcard c1 ) by Def6, Th27;
hence Card {} <` nextcard c1 by ORDINAL1:22;
end;

theorem Th34: :: CARD_1:34
for b1, b2 being set holds
( Card b1 = Card b2 implies nextcard b1 = nextcard b2 )
proof
let c1, c2 be set ;
assume E17: Card c1 = Card c2 ;
( Card c1 <` nextcard c1 & ( for b1 being Cardinal holds
( Card c1 <` b1 implies nextcard c1 <=` b1 ) ) ) by Def6;
hence nextcard c1 = nextcard c2 by E17, Def6;
end;

theorem Th35: :: CARD_1:35
for b1, b2 being set holds
( b1,b2 are_equipotent implies nextcard b1 = nextcard b2 )
proof
let c1, c2 be set ;
assume c1,c2 are_equipotent ;
then Card c1 = Card c2 by Th21;
hence nextcard c1 = nextcard c2 by Th34;
end;

theorem Th36: :: CARD_1:36
for b1 being Ordinal holds b1 in nextcard b1
proof
let c1 be Ordinal;
assume not c1 in nextcard c1 ;
then ( nextcard c1 c= c1 & c1, Card c1 are_equipotent ) by Def5, ORDINAL1:26;
then ( Card (nextcard c1) <=` Card c1 & Card (nextcard c1) = nextcard c1 & nextcard (Card c1) = nextcard c1 & Card c1 <` nextcard (Card c1) ) by Def5, Th27, Th32, Th35;
hence not verum by ORDINAL1:7;
end;

definition
let c1 be Cardinal;
attr a1 is limit means :Def7: :: CARD_1:def 7
for b1 being Cardinal holds
not a1 = nextcard b1;
end;

:: deftheorem Def7 defines limit CARD_1:def 7 :
for b1 being Cardinal holds
( b1 is limit iff for b2 being Cardinal holds
not b1 = nextcard b2 );

notation
let c1 be Cardinal;
synonym c1 is_limit_cardinal for limit c1;
end;

definition
let c1 be Ordinal;
func alef c1 -> set means :Def8: :: CARD_1:def 8
ex b1 being T-Sequence st
( a2 = last b1 & dom b1 = succ a1 & b1 . {} = Card NAT & ( for b2 being Ordinal holds
( succ b2 in succ a1 implies b1 . (succ b2) = nextcard (union {(b1 . b2)}) ) ) & ( for b2 being Ordinal holds
( b2 in succ a1 & b2 <> {} & b2 is_limit_ordinal implies b1 . b2 = Card (sup (b1 | b2)) ) ) );
correctness
existence
ex b1 being set ex b2 being T-Sequence st
( b1 = last b2 & dom b2 = succ c1 & b2 . {} = Card NAT & ( for b3 being Ordinal holds
( succ b3 in succ c1 implies b2 . (succ b3) = nextcard (union {(b2 . b3)}) ) ) & ( for b3 being Ordinal holds
( b3 in succ c1 & b3 <> {} & b3 is_limit_ordinal implies b2 . b3 = Card (sup (b2 | b3)) ) ) );
uniqueness
for b1, b2 being set holds
( ex b3 being T-Sequence st
( b1 = last b3 & dom b3 = succ c1 & b3 . {} = Card NAT & ( for b4 being Ordinal holds
( succ b4 in succ c1 implies b3 . (succ b4) = nextcard (union {(b3 . b4)}) ) ) & ( for b4 being Ordinal holds
( b4 in succ c1 & b4 <> {} & b4 is_limit_ordinal implies b3 . b4 = Card (sup (b3 | b4)) ) ) ) & ex b3 being T-Sequence st
( b2 = last b3 & dom b3 = succ c1 & b3 . {} = Card NAT & ( for b4 being Ordinal holds
( succ b4 in succ c1 implies b3 . (succ b4) = nextcard (union {(b3 . b4)}) ) ) & ( for b4 being Ordinal holds
( b4 in succ c1 & b4 <> {} & b4 is_limit_ordinal implies b3 . b4 = Card (sup (b3 | b4)) ) ) ) implies b1 = b2 );
proof
deffunc H1( Ordinal, set ) -> Cardinal = nextcard (union {a2});
deffunc H2( Ordinal, T-Sequence) -> Cardinal = Card (sup a2);
set c2 = Card NAT ;
thus ( ex b1 being set ex b2 being T-Sequence st
( b1 = last b2 & dom b2 = succ c1 & b2 . {} = Card NAT & ( for b3 being Ordinal holds
( succ b3 in succ c1 implies b2 . (succ b3) = H1(b3,b2 . b3) ) ) & ( for b3 being Ordinal holds
( b3 in succ c1 & b3 <> {} & b3 is_limit_ordinal implies b2 . b3 = H2(b3,b2 | b3) ) ) ) & ( for b1, b2 being set holds
( ex b3 being T-Sequence st
( b1 = last b3 & dom b3 = succ c1 & b3 . {} = Card NAT & ( for b4 being Ordinal holds
( succ b4 in succ c1 implies b3 . (succ b4) = H1(b4,b3 . b4) ) ) & ( for b4 being Ordinal holds
( b4 in succ c1 & b4 <> {} & b4 is_limit_ordinal implies b3 . b4 = H2(b4,b3 | b4) ) ) ) & ex b3 being T-Sequence st
( b2 = last b3 & dom b3 = succ c1 & b3 . {} = Card NAT & ( for b4 being Ordinal holds
( succ b4 in succ c1 implies b3 . (succ b4) = H1(b4,b3 . b4) ) ) & ( for b4 being Ordinal holds
( b4 in succ c1 & b4 <> {} & b4 is_limit_ordinal implies b3 . b4 = H2(b4,b3 | b4) ) ) ) implies b1 = b2 ) ) ) from ORDINAL2:sch 7();
end;
end;

:: deftheorem Def8 defines alef CARD_1:def 8 :
for b1 being Ordinal
for b2 being set holds
( b2 = alef b1 iff ex b3 being T-Sequence st
( b2 = last b3 & dom b3 = succ b1 & b3 . {} = Card NAT & ( for b4 being Ordinal holds
( succ b4 in succ b1 implies b3 . (succ b4) = nextcard (union {(b3 . b4)}) ) ) & ( for b4 being Ordinal holds
( b4 in succ b1 & b4 <> {} & b4 is_limit_ordinal implies b3 . b4 = Card (sup (b3 | b4)) ) ) ) );

E20: now
deffunc H1( Ordinal) -> set = alef a1;
deffunc H2( Ordinal, set ) -> Cardinal = nextcard (union {a2});
deffunc H3( Ordinal, T-Sequence) -> Cardinal = Card (sup a2);
E21: for b1 being Ordinal
for b2 being set holds
( b2 = H1(b1) iff ex b3 being T-Sequence st
( b2 = last b3 & dom b3 = succ b1 & b3 . {} = Card NAT & ( for b4 being Ordinal