let M be Cardinal; :: thesis: ( not M is finite implies ex A being Ordinal st M = alef A )
defpred S₁[ set ] means ( not $1 is finite implies ex A being Ordinal st $1 = alef A );
A1: for K being Cardinal st S₁[K] holds
S₁[ nextcard K]

proof

let K be Cardinal; :: thesis: ( S₁[K] implies S₁[ nextcard K] )
assume that
A2: S₁[K] and
A3: not nextcard K is finite ; :: thesis: ex A being Ordinal st nextcard K = alef A

now

assume K is finite ; :: thesis: contradiction
then reconsider K9 = K as finite set ;
card K = K by CARD_1:def 2;
then nextcard K = card ((card K9) + 1) by NAT_1:42;
hence contradiction by A3; :: thesis: verum

end;

then consider A being Ordinal such that
A4: K = alef A by A2;
take succ A ; :: thesis: nextcard K = alef (succ A)
thus nextcard K = alef (succ A) by A4, CARD_1:19; :: thesis: verum

end;

A5: for K being Cardinal st K <> {} & K is limit_cardinal & ( for N being Cardinal st N in K holds
S₁[N] ) holds
S₁[K]

proof

let K be Cardinal; :: thesis: ( K <> {} & K is limit_cardinal & ( for N being Cardinal st N in K holds
S₁[N] ) implies S₁[K] )
deffunc H₁( Ordinal) -> set = alef $1;
defpred S₂[ set , set ] means ex A being Ordinal st
( $1 = alef A & $2 = A );
assume that
K <> {} and
A6: K is limit_cardinal and
A7: for N being Cardinal st N in K holds
S₁[N] and
A8: not K is finite ; :: thesis: ex A being Ordinal st K = alef A
defpred S₃[ set ] means ex N being Cardinal st
( N = $1 & not N is finite );
consider X being set such that
A9: for x being set holds
( x in X iff ( x in K & S₃[x] ) ) from XBOOLE_0:sch 1();
A10: for x being set st x in X holds
ex y being set st S₂[x,y]

proof

let x be set ; :: thesis: ( x in X implies ex y being set st S₂[x,y] )
assume A11: x in X ; :: thesis: ex y being set st S₂[x,y]
then consider N being Cardinal such that
A12: N = x and
A13: not N is finite by A9;
N in K by A9, A11, A12;
then ex A being Ordinal st x = alef A by A7, A12, A13;
hence ex y being set st S₂[x,y] ; :: thesis: verum

end;

consider f being Function such that
A14: ( dom f = X & ( for x being set st x in X holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A10);

now

let x be set ; :: thesis: ( x in rng f implies ( x is Ordinal & x c= rng f ) )
assume x in rng f ; :: thesis: ( x is Ordinal & x c= rng f )
then consider y being set such that
A15: y in X and
A16: x = f . y by A14, FUNCT_1:def 3;
consider A being Ordinal such that
A17: y = alef A and
A18: x = A by A14, A15, A16;
thus x is Ordinal by A18; :: thesis: x c= rng f
thus x c= rng f :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in rng f )
assume A19: z in x ; :: thesis: z in rng f
then reconsider z9 = z as Ordinal by A18;
A20: alef z9 in alef A by A18, A19, CARD_1:21;
alef A in K by A9, A15, A17;
then A21: alef z9 in K by A20, ORDINAL1:10;
not alef z9 is finite by Th11;
then A22: alef z9 in X by A9, A21;
then ex A being Ordinal st
( alef z9 = alef A & f . (alef z9) = A ) by A14;
then z9 = f . (alef z9) by CARD_1:22;
hence z in rng f by A14, A22, FUNCT_1:def 3; :: thesis: verum

end;

end;

then reconsider A = rng f as Ordinal by ORDINAL1:19;
consider L being T-Sequence such that
A23: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H₁(B) ) ) from ORDINAL2:sch 2();

now

let B be Ordinal; :: thesis: ( B in A implies succ B in A )
assume B in A ; :: thesis: succ B in A
then consider x being set such that
A24: x in X and
A25: B = f . x by A14, FUNCT_1:def 3;
consider C being Ordinal such that
A26: x = alef C and
A27: B = C by A14, A24, A25;
A28: alef (succ C) = nextcard (alef C) by CARD_1:19;
alef C in K by A9, A24, A26;
then A29: alef (succ C) c= K by A28, CARD_3:90;
alef (succ C) <> K by A6, A28, CARD_1:def 4;
then A30: alef (succ C) in K by A29, CARD_1:3;
not alef (succ C) is finite by Th11;
then A31: alef (succ C) in X by A9, A30;
then consider D being Ordinal such that
A32: alef (succ C) = alef D and
A33: f . (alef (succ C)) = D by A14;
succ C = D by A32, CARD_1:22;
hence succ B in A by A14, A27, A31, A33, FUNCT_1:def 3; :: thesis: verum

end;

then A is limit_ordinal by ORDINAL1:28;
then A34: ( A = {} or alef A = card (sup L) ) by A23, CARD_1:20;
take A ; :: thesis: K = alef A
sup L c= K

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sup L or x in K )
assume A35: x in sup L ; :: thesis: x in K
then reconsider x9 = x as Ordinal ;
consider C being Ordinal such that
A36: C in rng L and
A37: x9 c= C by A35, ORDINAL2:21;
consider y being set such that
A38: y in dom L and
A39: C = L . y by A36, FUNCT_1:def 3;
reconsider y = y as Ordinal by A38;
A40: C = alef y by A23, A38, A39;
consider z being set such that
A41: z in dom f and
A42: y = f . z by A23, A38, FUNCT_1:def 3;
ex D being Ordinal st
( z = alef D & y = D ) by A14, A41, A42;
then C in K by A9, A14, A40, A41;
hence x in K by A37, ORDINAL1:12; :: thesis: verum

end;

then card (sup L) c= card K by CARD_1:11;
then A43: card (sup L) c= K by CARD_1:def 2;

now

per cases ( A = {} or A <> {} ) ;

case A = {} ; :: thesis: K = omega

then not omega in X by A14, RELAT_1:42;
then not omega in K by A9;
then A44: K c= omega by CARD_1:4;
omega c= K by A8, CARD_3:85;
hence K = omega by A44, XBOOLE_0:def 10; :: thesis: verum

end;

case A45: A <> {} ; :: thesis: not K <> alef A

assume K <> alef A ; :: thesis: contradiction
then A46: card (sup L) in K by A34, A43, A45, CARD_1:3;
not alef A is finite by Th11;
then A47: card (sup L) in X by A9, A34, A45, A46;
then consider B being Ordinal such that
A48: card (sup L) = alef B and
A49: f . (card (sup L)) = B by A14;
A = B by A34, A45, A48, CARD_1:22;
then A in A by A14, A47, A49, FUNCT_1:def 3;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence K = alef A by CARD_1:46; :: thesis: verum

end;

A50: S₁[ {} ] ;
for M being Cardinal holds S₁[M] from CARD_1:sch 1(A50, A1, A5);
hence ( not M is finite implies ex A being Ordinal st M = alef A ) ; :: thesis: verum