let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
deffunc H₁( Ordinal) -> set = Rank $1;
assume that
A1: A <> {} and
A2: A is limit_ordinal and
A3: 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 that
A4: W is Tarski and
A5: A in On W ; :: thesis: ( card (Rank A) in card W & Rank A in W )
consider L being T-Sequence such that
A6: ( 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
A7: ( dom F = A & ( for x being set st x in A holds
F . x = H₂(x) ) ) from CARD_3:sch 1();
A8: 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
A9: x = f and
A10: dom f = dom F and
A11: 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

A12: A in W by A5, ORDINAL1:def 10;
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
A13: y in dom f and
A14: z = f . y by FUNCT_1:def 5;
reconsider y = y as Ordinal by A7, A10, A13;
A15: f . y in F . y by A10, A11, A13;
y c= A by A7, A10, A13, ORDINAL1:def 2;
then y in W by A4, A12, CLASSES1:def 1;
then A16: y in On W by ORDINAL1:def 10;
L . y = Rank y by A6, A7, A10, A13;
then L . y in W by A3, A4, A7, A10, A13, A16;
then bool (L . y) in W by A4, CLASSES1:def 2;
then A17: card (bool (L . y)) in W by A4, Th12;
F . y = card (bool (L . y)) by A7, A10, A13;
then F . y c= W by A4, A17, Th6;
hence z in W by A14, A15; :: thesis: verum

end;

hence x in Funcs A,W by A7, A9, A10, FUNCT_2:def 2; :: thesis: verum

end;

A18: Product F = card (product F) by CARD_3:def 8;
A19: A in W by A5, ORDINAL1:def 10;
then A c= W by A4, Th6;
then Funcs A,W c= W by A4, A19, Th23;
then product F c= W by A8, XBOOLE_1:1;
then A20: Product F c= card W by A18, CARD_1:27;
A21: 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 )
A22: card (L . x) in card (bool (L . x)) by CARD_1:30;
assume x in dom (Card L) ; :: thesis: (Card L) . x in F . x
then A23: x in dom L by CARD_3:def 2;
then F . x = card (bool (L . x)) by A6, A7;
hence (Card L) . x in F . x by A23, A22, CARD_3:def 2; :: thesis: verum

end;

dom (Card L) = dom L by CARD_3:def 2;
then A24: Sum (Card L) in Product F by A6, A7, A21, CARD_3:56;
A25: 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
A26: B in A and
A27: x in Rank B by A1, A2, CLASSES1:35;
B c= A by A26, ORDINAL1:def 2;
then B in W by A4, A19, CLASSES1:def 1;
then B in On W by ORDINAL1:def 10;
then Rank B c= W by A3, A4, A26, Th8;
hence x in W by A27; :: thesis: verum

end;

A28: Rank A = Union L by A2, A6, Th25;
hence card (Rank A) in card W by A24, A20, CARD_3:54, ORDINAL1:22; :: thesis: Rank A in W
card (Rank A) in Product F by A28, A24, CARD_3:54, ORDINAL1:22;
hence Rank A in W by A4, A20, A25, CLASSES1:2; :: thesis: verum