let W be Universe; 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; ( 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) ) )
; 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,(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 ;
( e in WFF implies ex u being object st
( u in Funcs ((On W),(On W)) & S2[e,u] ) )
assume
e in WFF
;
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,
(Union L) ! va |= H iff
L . a,
va |= H ) ) )
by A1, A2, ZF_REFLE:20;
reconsider u =
phi as
set ;
take
u
;
( u in Funcs ((On W),(On W)) & S2[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;
S2[e,u]
take
H
;
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
;
( 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;
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 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
; ( 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; 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; ( phi . a = a & {} <> a implies L . a is_elementary_subsystem_of Union L )
assume that
A10:
phi . a = a
and
A11:
{} <> a
; L . a is_elementary_subsystem_of Union L
thus
L . a c= Union L
by ZF_REFLE:16; ZFREFLE1:def 3 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; 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); ( 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 S3[ 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
S3[b] ) holds
S3[a]
proof
let a be
Ordinal of
W;
( 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 <> {}
;
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;
ORDINAL1:def 5 ( not A in xi . a or A in phi . a )
assume A25:
A in xi . a
;
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;
verum
end;
A36:
for a being Ordinal of W st S3[a] holds
S3[ succ a]
proof
let a be
Ordinal of
W;
( 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 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
(
S3[
a] implies
S3[
succ a] )
by A38, ORDINAL1:def 2;
verum
end;
A39:
S3[ 0-element_of W]
;
for a being Ordinal of W holds S3[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; verum