let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A1: ( A <> {} & A is limit_ordinal ) and
A2: for B being Ordinal st B in A holds
S₁[B] ; :: thesis: S₁[A]
let W be set ; :: thesis: ( W is Tarski & A in On W implies ( card (Rank A) in card W & Rank A in W ) )
assume A3: ( W is Tarski & A in On W ) ; :: thesis: ( card (Rank A) in card W & Rank A in W )
then A4: W is subset-closed ;
deffunc H₁( Ordinal) -> set = Rank $1;
consider L being T-Sequence such that
A5: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H₁(B) ) ) from ORDINAL2:sch 2();
deffunc H₂( set ) -> set = card (bool (L . $1));
consider F being Cardinal-Function such that
A6: ( dom F = A & ( for x being set st x in A holds
F . x = H₂(x) ) ) from CARD_3:sch 1();
A7: for x being set st x in dom (Card L) holds
(Card L) . x in F . x

proof

let x be set ; :: thesis: ( x in dom (Card L) implies (Card L) . x in F . x )
assume x in dom (Card L) ; :: thesis: (Card L) . x in F . x
then x in dom L by CARD_3:def 2;
then ( F . x = card (bool (L . x)) & card (L . x) in card (bool (L . x)) & card (L . x) = (Card L) . x ) by A5, A6, CARD_1:30, CARD_3:def 2;
hence (Card L) . x in F . x ; :: thesis: verum

end;

( dom (Card L) = dom L & Rank A = Union L ) by A1, A5, Th25, CARD_3:def 2;
then A8: ( card (Rank A) c= Sum (Card L) & Sum (Card L) in Product F ) by A5, A6, A7, CARD_3:54, CARD_3:56;
then A9: card (Rank A) in Product F by ORDINAL1:22;
A10: product F c= Funcs A,W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product F or x in Funcs A,W )
assume x in product F ; :: thesis: x in Funcs A,W
then consider f being Function such that
A11: ( x = f & dom f = dom F & ( for x being set st x in dom F holds
f . x in F . x ) ) by CARD_3:def 5;
rng f c= W

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in W )
assume z in rng f ; :: thesis: z in W
then consider y being set such that
A12: ( y in dom f & z = f . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A6, A11, A12;
( y c= A & A in W ) by A3, A6, A11, A12, ORDINAL1:def 2, ORDINAL1:def 10;
then A13: ( f . y in F . y & F . y = F . y & F . y = card (bool (L . y)) & L . y = Rank y & L . y = L . y & y in W ) by A4, A5, A6, A11, A12, CLASSES1:def 1;
then ( S₁[y] & y in On W ) by A2, A6, A11, A12, ORDINAL1:def 10;
then L . y in W by A3, A13;
then bool (L . y) in W by A3, CLASSES1:def 2;
then ( card (bool (L . y)) = card (bool (L . y)) & card (bool (L . y)) in W ) by A3, Th12;
then F . y c= W by A3, A13, Th6;
hence z in W by A12, A13; :: thesis: verum

end;

hence x in Funcs A,W by A6, A11, FUNCT_2:def 2; :: thesis: verum

end;

A14: A in W by A3, ORDINAL1:def 10;
then A c= W by A3, Th6;
then Funcs A,W c= W by A3, A14, Th23;
then ( product F c= W & Product F = card (product F) ) by A10, CARD_3:def 8, XBOOLE_1:1;
then A15: Product F c= card W by CARD_1:27;
hence card (Rank A) in card W by A8, ORDINAL1:22; :: thesis: Rank A in W
Rank A c= W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Rank A or x in W )
assume x in Rank A ; :: thesis: x in W
then consider B being Ordinal such that
A16: ( B in A & x in Rank B ) by A1, CLASSES1:35;
B c= A by A16, ORDINAL1:def 2;
then B in W by A4, A14, CLASSES1:def 1;
then B in On W by ORDINAL1:def 10;
then ( Rank B in W & Rank B is epsilon-transitive ) by A2, A3, A16;
then Rank B c= W by A4, Th8;
hence x in W by A16; :: thesis: verum

end;

hence Rank A in W by A3, A9, A15, CLASSES1:2; :: thesis: verum