let a be Aleph; :: thesis: ( cf a in a implies ex xi being Ordinal-Sequence st
( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi ) )
a is_cofinal_with cf a by Def1;
then consider xi being Ordinal-Sequence such that
A1: dom xi = cf a and
A2: rng xi c= a and
xi is increasing and
A3: a = sup xi ;
deffunc H₁( Sequence) -> set = (nextcard (xi . (dom $1))) \/ (nextcard (sup $1));
consider phi being Sequence such that
A4: ( dom phi = cf a & ( for A being Ordinal
for psi being Sequence st A in cf a & psi = phi | A holds
phi . A = H₁(psi) ) ) from ORDINAL1:sch 4();
phi is Ordinal-yielding

proof

take sup (rng phi) ; :: according to ORDINAL2:def 4 :: thesis: rng phi c= sup (rng phi)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in sup (rng phi) )
assume A5: x in rng phi ; :: thesis: x in sup (rng phi)
then consider y being object such that
A6: y in dom phi and
A7: x = phi . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A6;
y c= dom phi by A6, ORDINAL1:def 2;
then dom (phi | y) = y by RELAT_1:62;
then x = (nextcard (xi . y)) \/ (nextcard (sup (phi | y))) by A4, A6, A7;
hence x in sup (rng phi) by A5, ORDINAL2:19; :: thesis: verum

end;

then reconsider phi = phi as Ordinal-Sequence ;
defpred S₁[ Ordinal] means ( $1 in cf a implies phi . $1 in a );
assume cf a in a ; :: thesis: ex xi being Ordinal-Sequence st
( dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi )
then A8: a is limit_cardinal by Th27;

A9: now :: thesis: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume A10: for B being Ordinal st B in A holds
S₁[B] ; :: thesis: S₁[A]
thus S₁[A] :: thesis: verum

proof

assume A11: A in cf a ; :: thesis: phi . A in a
then A12: card A in cf a by CARD_1:9;
A c= dom phi by A4, A11, ORDINAL1:def 2;
then A13: dom (phi | A) = A by RELAT_1:62;
then phi . A = (nextcard (xi . A)) \/ (nextcard (sup (phi | A))) by A4, A11;
then A14: ( phi . A = nextcard (xi . A) or phi . A = nextcard (sup (phi | A)) ) by ORDINAL3:12;
A15: rng (phi | A) c= a

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (phi | A) or x in a )
assume x in rng (phi | A) ; :: thesis: x in a
then consider y being object such that
A16: y in dom (phi | A) and
A17: x = (phi | A) . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A16;
( x = phi . y & y in cf a ) by A11, A13, A16, A17, FUNCT_1:47, ORDINAL1:10;
hence x in a by A10, A13, A16; :: thesis: verum

end;

(phi | A) .: A = rng (phi | A) by A13, RELAT_1:113;
then card (rng (phi | A)) in cf a by A12, CARD_1:67, ORDINAL1:12;
then sup (rng (phi | A)) in a by A15, Th25;
then card (sup (phi | A)) in a by CARD_1:9;
then A18: nextcard (card (sup (phi | A))) c= a by CARD_3:90;
xi . A in rng xi by A1, A11, FUNCT_1:def 3;
then card (xi . A) in a by A2, CARD_1:9;
then A19: nextcard (card (xi . A)) c= a by CARD_3:90;
A20: ( nextcard (card (sup (phi | A))) <> a & nextcard (card (sup (phi | A))) = nextcard (sup (phi | A)) ) by A8, Th1;
( a <> nextcard (card (xi . A)) & nextcard (card (xi . A)) = nextcard (xi . A) ) by A8, Th1;
hence phi . A in a by A19, A18, A20, A14, CARD_1:3; :: thesis: verum

end;

end;

A21: for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A9);
A22: rng phi c= a

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in a )
assume x in rng phi ; :: thesis: x in a
then ex y being object st
( y in dom phi & x = phi . y ) by FUNCT_1:def 3;
hence x in a by A4, A21; :: thesis: verum

end;

take phi ; :: thesis: ( dom phi = cf a & rng phi c= a & phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi )
thus dom phi = cf a by A4; :: thesis: ( rng phi c= a & phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi )
thus rng phi c= a :: thesis: ( phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in a )
assume x in rng phi ; :: thesis: x in a
then ex y being object st
( y in dom phi & x = phi . y ) by FUNCT_1:def 3;
hence x in a by A4, A21; :: thesis: verum

end;

thus phi is increasing :: thesis: ( a = sup phi & phi is Cardinal-Function & not 0 in rng phi )

proof

let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom phi or phi . A in phi . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume that
A23: A in B and
A24: B in dom phi ; :: thesis: phi . A in phi . B
reconsider C = phi . A as Ordinal ;
A in dom phi by A23, A24, ORDINAL1:10;
then C in rng (phi | B) by A23, FUNCT_1:50;
then A25: C in sup (phi | B) by ORDINAL2:19;
sup (phi | B) in nextcard (sup (phi | B)) by CARD_1:18;
then A26: C in nextcard (sup (phi | B)) by A25, ORDINAL1:10;
phi . B = (nextcard (xi . (dom (phi | B)))) \/ (nextcard (sup (phi | B))) by A4, A24;
hence phi . A in phi . B by A26, XBOOLE_0:def 3; :: thesis: verum

end;

thus a c= sup phi :: according to XBOOLE_0:def 10 :: thesis: ( sup phi c= a & phi is Cardinal-Function & not 0 in rng phi )

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in a or x in sup phi )
assume x in a ; :: thesis: x in sup phi
then reconsider x = x as Element of a ;
consider A being Ordinal such that
A27: A in rng xi and
A28: x c= A by A3, ORDINAL2:21;
consider y being object such that
A29: y in dom xi and
A30: A = xi . y by A27, FUNCT_1:def 3;
reconsider y = y as Ordinal by A29;
y c= cf a by A1, A29, ORDINAL1:def 2;
then dom (phi | y) = y by A4, RELAT_1:62;
then ( A in nextcard A & phi . y = (nextcard A) \/ (nextcard (sup (phi | y))) ) by A1, A4, A29, A30, CARD_1:18;
then A in phi . y by XBOOLE_0:def 3;
then A31: A c= phi . y by ORDINAL1:def 2;
phi . y in rng phi by A1, A4, A29, FUNCT_1:def 3;
then phi . y in sup phi by ORDINAL2:19;
hence x in sup phi by A28, A31, ORDINAL1:12, XBOOLE_1:1; :: thesis: verum

end;

sup a = a by ORDINAL2:18;
hence sup phi c= a by A22, ORDINAL2:22; :: thesis: ( phi is Cardinal-Function & not 0 in rng phi )
phi is Cardinal-yielding

proof

let y be object ; :: according to CARD_3:def 1 :: thesis: ( not y in dom phi or phi . y is set )
assume A32: y in dom phi ; :: thesis: phi . y is set
then reconsider y = y as Ordinal ;
y c= dom phi by A32, ORDINAL1:def 2;
then dom (phi | y) = y by RELAT_1:62;
then phi . y = (nextcard (xi . y)) \/ (nextcard (sup (phi | y))) by A4, A32;
hence phi . y is set by ORDINAL3:12; :: thesis: verum

end;

hence phi is Cardinal-Function ; :: thesis: not 0 in rng phi
assume 0 in rng phi ; :: thesis: contradiction
then consider x being object such that
A33: x in dom phi and
A34: 0 = phi . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A33;
x c= dom phi by A33, ORDINAL1:def 2;
then dom (phi | x) = x by RELAT_1:62;
then 0 = (nextcard (xi . x)) \/ (nextcard (sup (phi | x))) by A4, A33, A34;
then ( 0 = nextcard (xi . x) or 0 = nextcard (sup (phi | x)) ) ;
hence contradiction by CARD_1:15; :: thesis: verum