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 S_{2}[ 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,(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)) & S_{2}[e,u] )

A5: ( dom Phi = WFF & rng Phi c= Funcs ((On W),(On W)) ) and

A6: for e being object st e in WFF holds

S_{2}[e,Phi . e]
from FUNCT_1:sch 6(A3);

reconsider Phi = Phi as Function of WFF,(Funcs ((On W),(On W))) by A5, FUNCT_2:def 1, RELSET_1:4;

[:omega,omega:] in W by A1, CLASSES2:61;

then bool [:omega,omega:] in W by CLASSES2:59;

then ( card WFF c= card (bool [:omega,omega:]) & card (bool [:omega,omega:]) in card W ) by CARD_1:11, CLASSES2:1, ZF_LANG1:134;

then consider phi being Ordinal-Sequence of W such that

A7: ( phi is increasing & phi is continuous ) and

phi . (0-element_of W) = 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 Th13, ORDINAL1:12;

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: L . a is_elementary_subsystem_of Union L

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,(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,(Union L) ! v |= H )

let va be Function of VAR,(L . a); :: thesis: ( L . a,va |= H iff Union L,(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,(Union L) ! va |= H1 iff L . a,va |= H1 ) by A6;

defpred S_{3}[ Ordinal] means ( $1 <> {} implies xi . $1 c= phi . $1 );

a in dom xi by ORDINAL4:34;

then A18: a c= xi . a by A15, ORDINAL4:10;

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

S_{3}[b] ) holds

S_{3}[a]
_{3}[a] holds

S_{3}[ succ a]
_{3}[ 0-element_of W]
;

for a being Ordinal of W holds S_{3}[a]
from ZF_REFLE:sch 4(A39, A36, A19);

then xi . a c= a by A10, A11;

then xi . a = a by A18;

hence ( L . a,va |= H iff Union L,(Union L) ! va |= H ) by A11, A13, A17; :: thesis: verum

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 S

( $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 ) ) );

A3: for e being object st e in WFF holds

ex u being object st

( u in Funcs ((On W),(On W)) & S

proof

consider Phi being Function such that
let e be object ; :: thesis: ( e in WFF implies ex u being object st

( u in Funcs ((On W),(On W)) & S_{2}[e,u] ) )

assume e in WFF ; :: thesis: ex u being object st

( u in Funcs ((On W),(On W)) & S_{2}[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,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A1, A2, ZF_REFLE:20;

reconsider u = phi as set ;

take u ; :: thesis: ( u in Funcs ((On W),(On W)) & S_{2}[e,u] )

( 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: S_{2}[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,(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,(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,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A4; :: thesis: verum

end;( u in Funcs ((On W),(On W)) & S

assume e in WFF ; :: thesis: ex u being object st

( u in Funcs ((On W),(On W)) & S

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,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A1, A2, ZF_REFLE:20;

reconsider u = phi as set ;

take u ; :: thesis: ( u in Funcs ((On W),(On W)) & S

( 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: S

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,(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,(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,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A4; :: thesis: verum

A5: ( dom Phi = WFF & rng Phi c= Funcs ((On W),(On W)) ) and

A6: for e being object st e in WFF holds

S

reconsider Phi = Phi as Function of WFF,(Funcs ((On W),(On W))) by A5, FUNCT_2:def 1, RELSET_1:4;

[:omega,omega:] in W by A1, CLASSES2:61;

then bool [:omega,omega:] in W by CLASSES2:59;

then ( card WFF c= card (bool [:omega,omega:]) & card (bool [:omega,omega:]) in card W ) by CARD_1:11, CLASSES2:1, ZF_LANG1:134;

then consider phi being Ordinal-Sequence of W such that

A7: ( phi is increasing & phi is continuous ) and

phi . (0-element_of W) = 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 Th13, ORDINAL1:12;

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: L . a is_elementary_subsystem_of Union L

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,(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,(Union L) ! v |= H )

let va be Function of VAR,(L . a); :: thesis: ( L . a,va |= H iff Union L,(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,(Union L) ! va |= H1 iff L . a,va |= H1 ) by A6;

defpred S

a in dom xi by ORDINAL4:34;

then A18: a c= xi . a by A15, ORDINAL4:10;

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

S

S

proof

A36:
for a being Ordinal of W st S
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

S_{3}[b] ) implies S_{3}[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 A16, A20, A21;

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 A23, ORDINAL1:def 2;

then A26: dom (xi | a) = a by RELAT_1:62;

xi | a is increasing by A15, ORDINAL4:15;

then xi . a = sup (xi | a) by A20, A21, A26, A24, ORDINAL4:8

.= sup (rng (xi | a)) ;

then consider B being Ordinal such that

A27: B in rng (xi | a) and

A28: A c= B by A25, ORDINAL2:21;

consider e being object such that

A29: e in dom (xi | a) and

A30: B = (xi | a) . e by A27, FUNCT_1:def 3;

reconsider e = e as Ordinal by A29;

a in On W by ZF_REFLE:7;

then e in On W by A26, A29, ORDINAL1:10;

then reconsider e = e as Ordinal of W by ZF_REFLE:7;

A31: succ e in a by A21, A26, A29, ORDINAL1:28;

( e in succ e & succ e in dom xi ) by ORDINAL1:6, ORDINAL4:34;

then A32: xi . e in xi . (succ e) by A15;

B = xi . e by A29, A30, FUNCT_1:47;

then A33: A in xi . (succ e) by A28, A32, ORDINAL1:12;

succ e in dom phi by ORDINAL4:34;

then A34: phi . (succ e) in rng (phi | a) by A31, FUNCT_1:50;

phi . a = sup (phi | a) by A9, A20, A21

.= sup (rng (phi | a)) ;

then A35: phi . (succ e) in phi . a by A34, ORDINAL2:19;

xi . (succ e) c= phi . (succ e) by A22, A31;

hence A in phi . a by A35, A33, ORDINAL1:10; :: thesis: verum

end;S

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 A16, A20, A21;

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 A23, ORDINAL1:def 2;

then A26: dom (xi | a) = a by RELAT_1:62;

xi | a is increasing by A15, ORDINAL4:15;

then xi . a = sup (xi | a) by A20, A21, A26, A24, ORDINAL4:8

.= sup (rng (xi | a)) ;

then consider B being Ordinal such that

A27: B in rng (xi | a) and

A28: A c= B by A25, ORDINAL2:21;

consider e being object such that

A29: e in dom (xi | a) and

A30: B = (xi | a) . e by A27, FUNCT_1:def 3;

reconsider e = e as Ordinal by A29;

a in On W by ZF_REFLE:7;

then e in On W by A26, A29, ORDINAL1:10;

then reconsider e = e as Ordinal of W by ZF_REFLE:7;

A31: succ e in a by A21, A26, A29, ORDINAL1:28;

( e in succ e & succ e in dom xi ) by ORDINAL1:6, ORDINAL4:34;

then A32: xi . e in xi . (succ e) by A15;

B = xi . e by A29, A30, FUNCT_1:47;

then A33: A in xi . (succ e) by A28, A32, ORDINAL1:12;

succ e in dom phi by ORDINAL4:34;

then A34: phi . (succ e) in rng (phi | a) by A31, FUNCT_1:50;

phi . a = sup (phi | a) by A9, A20, A21

.= sup (rng (phi | a)) ;

then A35: phi . (succ e) in phi . a by A34, ORDINAL2:19;

xi . (succ e) c= phi . (succ e) by A22, A31;

hence A in phi . a by A35, A33, ORDINAL1:10; :: thesis: verum

S

proof

A39:
S
let a be Ordinal of W; :: thesis: ( S_{3}[a] implies S_{3}[ succ a] )

succ a in {(succ a)} by TARSKI:def 1;

then A37: [H,(succ a)] in [:WFF,{(succ a)}:] by A12, ZFMISC_1:87;

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 A5, A12, A14, FUNCT_5:38;

then xi . (succ a) in (uncurry Phi) .: [:WFF,{(succ a)}:] by A37, FUNCT_1:def 6;

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 ( S_{3}[a] implies S_{3}[ succ a] )
by A38, ORDINAL1:def 2; :: thesis: verum

end;succ a in {(succ a)} by TARSKI:def 1;

then A37: [H,(succ a)] in [:WFF,{(succ a)}:] by A12, ZFMISC_1:87;

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 A5, A12, A14, FUNCT_5:38;

then xi . (succ a) in (uncurry Phi) .: [:WFF,{(succ a)}:] by A37, FUNCT_1:def 6;

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 ( S

for a being Ordinal of W holds S

then xi . a c= a by A10, A11;

then xi . a = a by A18;

hence ( L . a,va |= H iff Union L,(Union L) ! va |= H ) by A11, A13, A17; :: thesis: verum