let W be Universe; :: thesis:
let L be DOMAIN-Sequence of ; :: thesis:
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 and
A3: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ; :: thesis:
defpred S₂[ set , set ] 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,(Union L) ! va |= H iff L . a,va |= H ) ) );
A4: for e being set st e in WFF holds
ex u being set st
( u in Funcs (On W),(On W) & S₂[e,u] )

proof

let e be set ; :: thesis:
assume e in WFF ; :: thesis:
then reconsider H = e as ZF-formula by ZF_LANG:14;
consider phi being Ordinal-Sequence of W such that
A5: ( 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,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A1, A2, A3, ZF_REFLE:29;
reconsider u = phi as set ;
take u ; :: thesis:
( dom phi = On W & rng phi c= On W ) by FUNCT_2:def 1, RELAT_1:def 19;
hence u in Funcs (On W),(On W) by FUNCT_2:def 2; :: thesis:
take H ; :: thesis:
take phi ; :: thesis:
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,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A5; :: thesis:

end;

consider Phi being Function such that
A6: ( dom Phi = WFF & rng Phi c= Funcs (On W),(On W) ) and
A7: for e being set st e in WFF holds
S₂[e,Phi . e] from WELLORD2:sch 1(A4);
reconsider Phi = Phi as Function of WFF ,(Funcs (On W),(On W)) by A6, FUNCT_2:def 1, RELSET_1:11;
( [:NAT ,NAT :],[:omega ,omega :] are_equipotent & [:omega ,omega :] in W ) by A1, CLASSES2:67;
then ( card (bool [:NAT ,NAT :]) = card (bool [:omega ,omega :]) & WFF c= bool [:NAT ,NAT :] & bool [:omega ,omega :] in W ) by CLASSES2:65, ZF_LANG1:146;
then ( card WFF c= card (bool [:omega ,omega :]) & card (bool [:omega ,omega :]) in card W ) by CARD_1:27, CLASSES2:1;
then card WFF in card W by ORDINAL1:22;
then consider phi being Ordinal-Sequence of W such that
A8: ( phi is increasing & phi is continuous ) and
phi . (0-element_of W) = 0-element_of W and
A9: for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF ,{(succ a)}:])) and
A10: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) by Th14;
take phi ; :: thesis:
thus ( phi is increasing & phi is continuous ) by A8; :: thesis:
let a be Ordinal of W; :: thesis:
assume A11: ( phi . a = a & {} <> a ) ; :: thesis:
thus L . a c= Union L by ZF_REFLE:24; :: according to ZFREFLE1:def 3 :: thesis:
let H be ZF-formula; :: thesis:
let va be Function of VAR ,(L . a); :: thesis:
set M = Union L;
A12: H in WFF by ZF_LANG:14;
then consider H1 being ZF-formula, xi being Ordinal-Sequence of W such that
A13: ( H = H1 & Phi . H = xi & xi is increasing & xi is continuous & ( for a being Ordinal of W st xi . a = a & {} <> a holds
for va being Function of VAR ,(L . a) holds
( Union L,(Union L) ! va |= H1 iff L . a,va |= H1 ) ) ) by A7;
A14: a in dom xi by ORDINAL4:36;
defpred S₃[ Ordinal] means ( $1 <> {} implies xi . $1 c= phi . $1 );
A15: S₃[ 0-element_of W] ;
A16: for a being Ordinal of W st S₃[a] holds
S₃[ succ a]

proof

let a be Ordinal of W; :: thesis:
( succ a in dom xi & succ a in {(succ a)} ) by ORDINAL4:36, TARSKI:def 1;
then ( [H,(succ a)] in dom (uncurry Phi) & (uncurry Phi) . H,(succ a) = xi . (succ a) & [H,(succ a)] in [:WFF ,{(succ a)}:] ) by A6, A12, A13, FUNCT_5:45, ZFMISC_1:106;
then xi . (succ a) in (uncurry Phi) .: [:WFF ,{(succ a)}:] by FUNCT_1:def 12;
then xi . (succ a) in {(phi . a)} \/ ((uncurry Phi) .: [:WFF ,{(succ a)}:]) by XBOOLE_0:def 3;
then ( xi . (succ a) in sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF ,{(succ a)}:])) & phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF ,{(succ a)}:])) ) by A9, ORDINAL2:27;
hence ( S₃[a] implies S₃[ succ a] ) by ORDINAL1:def 2; :: thesis:

end;

A17: 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
S₃[b] ) holds
S₃[a]

proof

let a be Ordinal of W; :: thesis:
assume that
A18: ( a <> 0-element_of W & a is limit_ordinal ) and
A19: for b being Ordinal of W st b in a & b <> {} holds
xi . b c= phi . b and
a <> {} ; :: thesis:
A21: phi . a = sup (phi | a) by A10, A18
.= sup (rng (phi | a)) ;
let A be Ordinal; :: according to ORDINAL1:def 5 :: thesis:
assume A22: A in xi . a ; :: thesis:
a in dom xi by ORDINAL4:36;
then A23: ( xi . a is_limes_of xi | a & xi | a is increasing & a c= dom xi ) by A13, A18, ORDINAL1:def 2, ORDINAL2:def 17, ORDINAL4:15;
then A24: ( dom (xi | a) = a & xi . a = lim (xi | a) ) by ORDINAL2:def 14, RELAT_1:91;
then xi . a = sup (xi | a) by A18, A23, ORDINAL4:8
.= sup (rng (xi | a)) ;
then consider B being Ordinal such that
A25: ( B in rng (xi | a) & A c= B ) by A22, ORDINAL2:29;
consider e being set such that
A26: ( e in dom (xi | a) & B = (xi | a) . e ) by A25, FUNCT_1:def 5;
reconsider e = e as Ordinal by A26;
a in On W by ZF_REFLE:8;
then e in On W by A24, A26, ORDINAL1:19;
then reconsider e = e as Ordinal of W by ZF_REFLE:8;
( succ e in a & succ e in dom phi ) by A18, A24, A26, ORDINAL1:41, ORDINAL4:36;
then ( succ e <> {} & succ e in a & e in succ e & phi . (succ e) in rng (phi | a) & succ e in dom xi ) by FUNCT_1:73, ORDINAL1:10, ORDINAL4:36;
then ( xi . (succ e) c= phi . (succ e) & xi . e in xi . (succ e) & phi . (succ e) in phi . a & B = xi . e ) by A13, A19, A21, A26, FUNCT_1:70, ORDINAL2:27, ORDINAL2:def 16;
then ( A in xi . (succ e) & xi . (succ e) in phi . a ) by A25, ORDINAL1:22;
hence A in phi . a by ORDINAL1:19; :: thesis:

end;

for a being Ordinal of W holds S₃[a] from ZF_REFLE:sch 4(A15, A16, A17);
then ( a c= xi . a & xi . a c= a ) by A11, A13, A14, ORDINAL4:10;
then xi . a = a by XBOOLE_0:def 10;
hence ( L . a,va |= H iff Union L,(Union L) ! va |= H ) by A11, A13; :: thesis: