let A, B be Ordinal; :: thesis: ( A in B iff aleph A in aleph B )
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]

proof

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

A4: now :: thesis: ( A in B & A in succ B implies aleph A in aleph (succ B) )

assume A in B ; :: thesis: ( A in succ B implies aleph A in aleph (succ B) )
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: verum

end;

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

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]

proof

let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
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: S₁[B]
let A be Ordinal; :: thesis: ( A in B implies aleph A in aleph B )
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: aleph A in aleph B
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: verum

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: ( aleph A in aleph B implies A in B )
assume A17: aleph A in aleph B ; :: thesis: A in B
then A18: aleph A <> aleph B ;
not B in A by A16, A17;
hence A in B by A18, ORDINAL1:14; :: thesis: verum