let W be Universe; :: thesis:
assume A1: omega in W ; :: thesis:
deffunc H₁( Ordinal, set ) -> set = Rank (succ $1);
deffunc H₂( Ordinal, set ) -> set = Rank $1;
consider L being T-Sequence such that
A2: ( dom L = On W & ( {} in On W implies L . {} = Rank (1-element_of W) ) ) and
A3: for A being Ordinal st succ A in On W holds
L . (succ A) = H₁(A,L . A) and
A4: for A being Ordinal st A in On W & A <> {} & A is limit_ordinal holds
L . A = H₂(A,L | A) from ORDINAL2:sch 5();
A5: ( 0-element_of W in On W & {} = 0-element_of W ) by ZF_REFLE:8;
A6: for a being Ordinal of W holds L . (succ a) = Rank (succ a)

proof

let a be Ordinal of W; :: thesis:
( succ a in On W & L . a = L . a ) by ZF_REFLE:8;
hence L . (succ a) = Rank (succ a) by A3; :: thesis:

end;

A7: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Rank a

proof

let a be Ordinal of W; :: thesis:
( a in On W & L | a = L | a ) by ZF_REFLE:8;
hence ( a <> {} & a is limit_ordinal implies L . a = Rank a ) by A4; :: thesis:

end;

A8: for a being Ordinal of W st a <> {} holds
L . a = Rank a

proof

let a be Ordinal of W; :: thesis:
A9: ( a is limit_ordinal or ex A being Ordinal st a = succ A ) by ORDINAL1:42;

now

given A being Ordinal such that A10: a = succ A ; :: thesis:
( A in a & a in On W ) by A10, ORDINAL1:10, ZF_REFLE:8;
then A in On W by ORDINAL1:19;
then reconsider A = A as Ordinal of W by ZF_REFLE:8;
L . (succ A) = Rank (succ A) by A6;
hence ( a <> {} implies L . a = Rank a ) by A10; :: thesis:

end;

hence ( a <> {} implies L . a = Rank a ) by A7, A9; :: thesis:

end;

rng L c= W

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in rng L ; :: thesis:
then consider u being set such that
A11: ( u in On W & e = L . u ) by A2, FUNCT_1:def 5;
reconsider u = u as Ordinal of W by A11, ZF_REFLE:8;
( Rank (1-element_of W) in W & Rank u in W ) by Th33;
hence e in W by A2, A8, A11; :: thesis:

end;

then reconsider L = L as T-Sequence of by RELAT_1:def 19;

now

assume {} in rng L ; :: thesis:
then consider e being set such that
A12: ( e in On W & {} = L . e ) by A2, FUNCT_1:def 5;
reconsider e = e as Ordinal of W by A12, ZF_REFLE:8;
( ( e = {} & 1-element_of W = {{} } ) or e <> {} ) by ORDINAL3:18;
then ( ( L . e = Rank (1-element_of W) & 1-element_of W <> {} ) or ( e <> {} & L . e = Rank e ) ) by A2, A8, ZF_REFLE:8;
hence contradiction by A12, Th34; :: thesis:

end;

then reconsider L = L as DOMAIN-Sequence of by A2, RELAT_1:def 9, ZF_REFLE:def 5;
A13: for a, b being Ordinal of W st a in b holds
L . a c= L . b

proof

let a, b be Ordinal of W; :: thesis:
assume A14: a in b ; :: thesis:
then A15: ( Rank a in Rank b & b <> {} & succ a c= b ) by CLASSES1:42, ORDINAL1:33;
A16: L . b = Rank b by A8, A14;
( L . a = Rank a or ( a = 0-element_of W & L . a = Rank (1-element_of W) & 1-element_of W = succ (0-element_of W) ) ) by A2, A5, A8;
hence L . a c= L . b by A15, A16, CLASSES1:43, ORDINAL1:def 2; :: thesis:

end;

for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a)

proof

let a be Ordinal of W; :: thesis:
assume A17: ( a <> {} & a is limit_ordinal ) ; :: thesis:
then A18: L . a = Rank a by A7;
A19: a in On W by ZF_REFLE:8;
thus L . a c= Union (L | a) :: according to XBOOLE_0:def 10 :: thesis:

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in L . a ; :: thesis:
then consider B being Ordinal such that
A20: ( B in a & e in Rank B ) by A17, A18, CLASSES1:35;
B in On W by A19, A20, ORDINAL1:19;
then reconsider B = B as Ordinal of W by ZF_REFLE:8;
( succ B in a & succ B in On W ) by A17, A20, ORDINAL1:41, ZF_REFLE:8;
then ( L . (succ B) = Rank (succ B) & L . (succ B) in rng (L | a) & Union (L | a) = union (rng (L | a)) ) by A2, A6, CARD_3:def 4, FUNCT_1:73;
then ( Rank B c= L . (succ B) & L . (succ B) c= Union (L | a) ) by CLASSES1:39, ZFMISC_1:92;
then Rank B c= Union (L | a) by XBOOLE_1:1;
hence e in Union (L | a) by A20; :: thesis:

end;

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in Union (L | a) ; :: thesis:
then e in union (rng (L | a)) by CARD_3:def 4;
then consider X being set such that
A21: ( e in X & X in rng (L | a) ) by TARSKI:def 4;
consider u being set such that
A22: ( u in dom (L | a) & X = (L | a) . u ) by A21, FUNCT_1:def 5;
reconsider u = u as Ordinal by A22;
A23: dom (L | a) c= a by RELAT_1:87;
then A24: ( X = L . u & u in a ) by A22, FUNCT_1:70;
u in On W by A19, A22, A23, ORDINAL1:19;
then reconsider u = u as Ordinal of W by ZF_REFLE:8;
L . u c= L . a by A13, A22, A23;
hence e in L . a by A21, A24; :: thesis:

end;

then consider phi being Ordinal-Sequence of W such that
A25: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L ) ) by A1, A13, Th32;
take phi ; :: thesis:
thus ( phi is increasing & phi is continuous ) by A25; :: thesis:
A26: Union L = W

proof

A27: Union L = union (rng L) by CARD_3:def 4;
thus Union L c= W ; :: according to XBOOLE_0:def 10 :: thesis:
let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in W ; :: thesis:
then ( e in Rank (On W) & On W <> {} & On W is limit_ordinal ) by CLASSES2:54, CLASSES2:55;
then consider A being Ordinal such that
A28: ( A in On W & e in Rank A ) by CLASSES1:35;
reconsider A = A as Ordinal of W by A28, ZF_REFLE:8;
( L . A = Rank A & L . A in rng L ) by A2, A8, A28, CLASSES1:33, FUNCT_1:def 5;
then Rank A c= Union L by A27, ZFMISC_1:92;
hence e in Union L by A28; :: thesis:

end;

let a be Ordinal of W; :: thesis:
let M be non empty set ; :: thesis:
assume A29: ( phi . a = a & {} <> a & M = Rank a ) ; :: thesis:
then M = L . a by A8;
hence M is_elementary_subsystem_of W by A25, A26, A29; :: thesis: