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 ) ) ;
then ( A in B or A = B ) by A3, ORDINAL1:11, ORDINAL1:22;
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:2;
hence UNIVERSE A in UNIVERSE (succ B) by A4, ORDINAL1:10; :: thesis: verum
end;
A5: for A being Ordinal st A <> 0 & 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 <> 0 & B is limit_ordinal & ( for B being Ordinal st B in B holds
S2[B] ) implies S2[B] )
assume that
A6: B <> 0 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 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:28;
then L . (succ A) = UNIVERSE (succ A) by A8;
then UNIVERSE (succ A) in rng L by A9, A8, FUNCT_1:def 3;
then A10: UNIVERSE (succ A) c= union (rng L) by ZFMISC_1:74;
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;
A12: UNIVERSE A in Tarski-Class (UNIVERSE A) by CLASSES1:2;
UNIVERSE (succ A) = Tarski-Class (UNIVERSE A) by Lm6;
hence UNIVERSE A in UNIVERSE B by A12, A11; :: thesis: verum
end;
A13: S2[ 0 ] ;
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 in A or B = A ) by A16, ORDINAL1:16;
hence contradiction by A14, A15; :: thesis: verum