let A, B be Ordinal; :: thesis: ( A in B iff UNIVERSE A in UNIVERSE B )
defpred S2[ Ordinal] means for A being Ordinal st A in $1 holds
UNIVERSE A in UNIVERSE $1;
A1: for B being Ordinal st S2[B] holds
S2[ succ B]
proof
let B be Ordinal; :: thesis: ( S2[B] implies S2[ succ B] )
assume A2: S2[B] ; :: thesis: S2[ succ B]
let A be Ordinal; :: thesis: ( A in succ B implies UNIVERSE A in UNIVERSE (succ B) )
assume A3: A in succ B ; :: thesis: UNIVERSE A in UNIVERSE (succ B)
( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def 8;
then ( A in B or A = B ) by A3, ORDINAL1:21, ORDINAL1:34;
then A4: ( UNIVERSE A in UNIVERSE B or UNIVERSE A = UNIVERSE B ) by A2;
UNIVERSE (succ B) = Tarski-Class (UNIVERSE B) by Lm6;
then UNIVERSE B in UNIVERSE (succ B) by CLASSES1:5;
hence UNIVERSE A in UNIVERSE (succ B) by A4, Th59; :: thesis: verum
end;
A5: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S2[B] ) holds
S2[A]
proof
let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for B being Ordinal st B in B holds
S2[B] ) implies S2[B] )
assume that
A6: B <> {} and
A7: B is limit_ordinal and
for C being Ordinal st C in B holds
for A being Ordinal st A in C holds
UNIVERSE A in UNIVERSE C ; :: thesis: S2[B]
let A be Ordinal; :: thesis: ( A in B implies UNIVERSE A in UNIVERSE B )
consider L being T-Sequence such that
A8: ( dom L = B & ( for C being Ordinal st C in B holds
L . C = H5(C) ) ) from ORDINAL2:sch 2();
 assume A in B ; :: thesis: UNIVERSE A in UNIVERSE B
then A9: succ A in B by A7, ORDINAL1:41;
then L . (succ A) = UNIVERSE (succ A) by A8;
then UNIVERSE (succ A) in rng L by A9, A8, FUNCT_1:def 5;
then A10: UNIVERSE (succ A) c= union (rng L) by ZFMISC_1:92;
UNIVERSE B = Universe_closure (Union L) by A6, A7, A8, Lm6
.= Universe_closure (union (rng L)) by CARD_3:def 4 ;
then union (rng L) c= UNIVERSE B by Def4;
then A11: UNIVERSE (succ A) c= UNIVERSE B by A10, XBOOLE_1:1;
A12: UNIVERSE A in Tarski-Class (UNIVERSE A) by CLASSES1:5;
UNIVERSE (succ A) = Tarski-Class (UNIVERSE A) by Lm6;
hence UNIVERSE A in UNIVERSE B by A12, A11; :: thesis: verum
end;
A13: S2[ {} ] ;
A14: for B being Ordinal holds S2[B] from ORDINAL2:sch 1(A13, A1, A5);
 hence ( A in B implies UNIVERSE A in UNIVERSE B ) ; :: thesis: ( UNIVERSE A in UNIVERSE B implies A in B )
assume that
A15: UNIVERSE A in UNIVERSE B and
A16: not A in B ; :: thesis: contradiction
( B c< A iff ( B c= A & B <> A ) ) by XBOOLE_0:def 8;
then ( B in A or B = A ) by A16, ORDINAL1:21, ORDINAL1:26;
hence contradiction by A14, A15; :: thesis: verum