let W be Universe; :: thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
ex phi being Ordinal-Sequence of W st
( 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 ) )

let L be DOMAIN-Sequence of W; :: thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) implies ex phi being Ordinal-Sequence of W st
( 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 ) ) )

assume that
A1: omega in W and
A2: ( ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) ) ; :: thesis: ex phi being Ordinal-Sequence of W st
( 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 ) )

set M = Union L;
defpred S2[ object , object ] means ex H being ZF-formula ex phi being Ordinal-Sequence of W st
( \$1 = H & \$2 = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,() ! va |= H iff L . a,va |= H ) ) );
A3: for e being object st e in WFF holds
ex u being object st
( u in Funcs ((On W),(On W)) & S2[e,u] )
proof
let e be object ; :: thesis: ( e in WFF implies ex u being object st
( u in Funcs ((On W),(On W)) & S2[e,u] ) )

assume e in WFF ; :: thesis: ex u being object st
( u in Funcs ((On W),(On W)) & S2[e,u] )

then reconsider H = e as ZF-formula by ZF_LANG:4;
consider phi being Ordinal-Sequence of W such that
A4: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,() ! va |= H iff L . a,va |= H ) ) ) by ;
reconsider u = phi as set ;
take u ; :: thesis: ( u in Funcs ((On W),(On W)) & S2[e,u] )
( dom phi = On W & rng phi c= On W ) by ;
hence u in Funcs ((On W),(On W)) by FUNCT_2:def 2; :: thesis: S2[e,u]
take H ; :: thesis: ex phi being Ordinal-Sequence of W st
( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,() ! va |= H iff L . a,va |= H ) ) )

take phi ; :: thesis: ( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,() ! va |= H iff L . a,va |= H ) ) )

thus ( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,() ! va |= H iff L . a,va |= H ) ) ) by A4; :: thesis: verum
end;
consider Phi being Function such that
A5: ( dom Phi = WFF & rng Phi c= Funcs ((On W),(On W)) ) and
A6: for e being object st e in WFF holds
S2[e,Phi . e] from reconsider Phi = Phi as Function of WFF,(Funcs ((On W),(On W))) by ;
[::] in W by ;
then bool in W by CLASSES2:59;
then ( card WFF c= card & card in card W ) by ;
then consider phi being Ordinal-Sequence of W such that
A7: ( phi is increasing & phi is continuous ) and
phi . () = 0-element_of W and
A8: for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) and
A9: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) by ;
take phi ; :: thesis: ( 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 ) )

thus ( phi is increasing & phi is continuous ) by A7; :: thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L

let a be Ordinal of W; :: thesis: ( phi . a = a & {} <> a implies L . a is_elementary_subsystem_of Union L )
assume that
A10: phi . a = a and
A11: {} <> a ; :: thesis:
thus L . a c= Union L by ZF_REFLE:16; :: according to ZFREFLE1:def 3 :: thesis: for H being ZF-formula
for v being Function of VAR,(L . a) holds
( L . a,v |= H iff Union L,() ! v |= H )

let H be ZF-formula; :: thesis: for v being Function of VAR,(L . a) holds
( L . a,v |= H iff Union L,() ! v |= H )

let va be Function of VAR,(L . a); :: thesis: ( L . a,va |= H iff Union L,() ! va |= H )
A12: H in WFF by ZF_LANG:4;
then consider H1 being ZF-formula, xi being Ordinal-Sequence of W such that
A13: H = H1 and
A14: Phi . H = xi and
A15: xi is increasing and
A16: xi is continuous and
A17: for a being Ordinal of W st xi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,() ! va |= H1 iff L . a,va |= H1 ) by A6;
defpred S3[ Ordinal] means ( \$1 <> {} implies xi . \$1 c= phi . \$1 );
a in dom xi by ORDINAL4:34;
then A18: a c= xi . a by ;
A19: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S3[b] ) holds
S3[a]
proof
let a be Ordinal of W; :: thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S3[b] ) implies S3[a] )

assume that
A20: a <> 0-element_of W and
A21: a is limit_ordinal and
A22: for b being Ordinal of W st b in a & b <> {} holds
xi . b c= phi . b and
a <> {} ; :: thesis: xi . a c= phi . a
A23: a in dom xi by ORDINAL4:34;
then xi . a is_limes_of xi | a by ;
then A24: xi . a = lim (xi | a) by ORDINAL2:def 10;
let A be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not A in xi . a or A in phi . a )
assume A25: A in xi . a ; :: thesis: A in phi . a
a c= dom xi by ;
then A26: dom (xi | a) = a by RELAT_1:62;
xi | a is increasing by ;
then xi . a = sup (xi | a) by
.= sup (rng (xi | a)) ;
then consider B being Ordinal such that
A27: B in rng (xi | a) and
A28: A c= B by ;
consider e being object such that
A29: e in dom (xi | a) and
A30: B = (xi | a) . e by ;
reconsider e = e as Ordinal by A29;
a in On W by ZF_REFLE:7;
then e in On W by ;
then reconsider e = e as Ordinal of W by ZF_REFLE:7;
A31: succ e in a by ;
( e in succ e & succ e in dom xi ) by ;
then A32: xi . e in xi . (succ e) by A15;
B = xi . e by ;
then A33: A in xi . (succ e) by ;
succ e in dom phi by ORDINAL4:34;
then A34: phi . (succ e) in rng (phi | a) by ;
phi . a = sup (phi | a) by A9, A20, A21
.= sup (rng (phi | a)) ;
then A35: phi . (succ e) in phi . a by ;
xi . (succ e) c= phi . (succ e) by ;
hence A in phi . a by ; :: thesis: verum
end;
A36: for a being Ordinal of W st S3[a] holds
S3[ succ a]
proof
let a be Ordinal of W; :: thesis: ( S3[a] implies S3[ succ a] )
succ a in {(succ a)} by TARSKI:def 1;
then A37: [H,(succ a)] in [:WFF,{(succ a)}:] by ;
succ a in dom xi by ORDINAL4:34;
then ( [H,(succ a)] in dom (uncurry Phi) & (uncurry Phi) . (H,(succ a)) = xi . (succ a) ) by ;
then xi . (succ a) in (uncurry Phi) .: [:WFF,{(succ a)}:] by ;
then xi . (succ a) in {(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:]) by XBOOLE_0:def 3;
then A38: xi . (succ a) in sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) by ORDINAL2:19;
phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) by A8;
hence ( S3[a] implies S3[ succ a] ) by ; :: thesis: verum
end;
A39: S3[ 0-element_of W] ;
for a being Ordinal of W holds S3[a] from then xi . a c= a by ;
then xi . a = a by A18;
hence ( L . a,va |= H iff Union L,() ! va |= H ) by ; :: thesis: verum