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
for H being ZF-formula 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
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
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 for H being ZF-formula 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
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) ) )
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)
; for H being ZF-formula 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
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
set M = Union L;
A4:
union (rng L) = Union L
by CARD_3:def 4;
defpred S1[ ZF-formula] means 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
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= $1 iff L . a,f |= $1 ) ) );
A5:
dom L = On W
by Def5;
A6:
for H being ZF-formula st H is universal & S1[ the_scope_of H] holds
S1[H]
proof
deffunc H1(
Ordinal of
W,
Ordinal-Sequence)
-> Ordinal of
W =
union $2,$1;
let H be
ZF-formula;
( H is universal & S1[ the_scope_of H] implies S1[H] )
set x0 =
bound_in H;
set H9 =
the_scope_of H;
defpred S2[
set ,
set ]
means ex
f being
Function of
VAR ,
(Union L) st
( $1
= f & ( ex
m being
Element of
Union L st
(
m in L . $2 &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or ( $2
= 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) );
assume
H is
universal
;
( not S1[ the_scope_of H] or S1[H] )
then A7:
H = All (bound_in H),
(the_scope_of H)
by ZF_LANG:62;
A8:
for
h being
Element of
Funcs VAR ,
(Union L) ex
a being
Ordinal of
W st
S2[
h,
a]
proof
let h be
Element of
Funcs VAR ,
(Union L);
ex a being Ordinal of W st S2[h,a]
reconsider f =
h as
Element of
Funcs VAR ,
(Union L) ;
reconsider f =
f as
Function of
VAR ,
(Union L) ;
now per cases
( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) or ex m being Element of Union L st Union L,f / (bound_in H),m |= 'not' (the_scope_of H) )
;
suppose A9:
ex
m being
Element of
Union L st
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H)
;
ex a being Ordinal of W st S2[h,a]thus
ex
a being
Ordinal of
W st
S2[
h,
a]
verumproof
consider m being
Element of
Union L such that A10:
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H)
by A9;
consider X being
set such that A11:
m in X
and A12:
X in rng L
by A4, TARSKI:def 4;
consider x being
set such that A13:
x in dom L
and A14:
X = L . x
by A12, FUNCT_1:def 5;
reconsider x =
x as
Ordinal by A13;
reconsider b =
x as
Ordinal of
W by A5, A13, ORDINAL1:def 10;
take
b
;
S2[h,b]
take
f
;
( h = f & ( ex m being Element of Union L st
( m in L . b & Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) or ( b = 0-element_of W & ( for m being Element of Union L holds not Union L,f / (bound_in H),m |= 'not' (the_scope_of H) ) ) ) )
thus
(
h = f & ( ex
m being
Element of
Union L st
(
m in L . b &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
b = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) )
by A10, A11, A14;
verum
end; end;
hence
ex
a being
Ordinal of
W st
S2[
h,
a]
;
verum
end;
consider rho being
Function such that A15:
dom rho = Funcs VAR ,
(Union L)
and A16:
for
h being
Element of
Funcs VAR ,
(Union L) ex
a being
Ordinal of
W st
(
a = rho . h &
S2[
h,
a] & ( for
b being
Ordinal of
W st
S2[
h,
b] holds
a c= b ) )
from ZF_REFLE:sch 1(A8);
defpred S3[
Ordinal of
W,
Ordinal of
W]
means $2
= sup (rho .: (Funcs VAR ,(L . $1)));
A17:
for
a being
Ordinal of
W ex
b being
Ordinal of
W st
S3[
a,
b]
proof
let a be
Ordinal of
W;
ex b being Ordinal of W st S3[a,b]
set X =
rho .: (Funcs VAR ,(L . a));
A18:
rho .: (Funcs VAR ,(L . a)) c= W
proof
let x be
set ;
TARSKI:def 3 ( not x in rho .: (Funcs VAR ,(L . a)) or x in W )
assume
x in rho .: (Funcs VAR ,(L . a))
;
x in W
then consider h being
set such that
h in dom rho
and A19:
h in Funcs VAR ,
(L . a)
and A20:
x = rho . h
by FUNCT_1:def 12;
Funcs VAR ,
(L . a) c= Funcs VAR ,
(Union L)
by Th24, FUNCT_5:63;
then reconsider h =
h as
Element of
Funcs VAR ,
(Union L) by A19;
ex
a being
Ordinal of
W st
(
a = rho . h & ex
f being
Function of
VAR ,
(Union L) st
(
h = f & ( ex
m being
Element of
Union L st
(
m in L . a &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
a = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) ) & ( for
b being
Ordinal of
W st ex
f being
Function of
VAR ,
(Union L) st
(
h = f & ( ex
m being
Element of
Union L st
(
m in L . b &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
b = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) ) holds
a c= b ) )
by A16;
hence
x in W
by A20;
verum
end;
Funcs omega ,
(L . a) in W
by A1, CLASSES2:67;
then A21:
card (Funcs omega ,(L . a)) in card W
by CLASSES2:1;
(
card VAR = card omega &
card (L . a) = card (L . a) )
by Th25, CARD_1:21;
then
card (Funcs VAR ,(L . a)) = card (Funcs omega ,(L . a))
by FUNCT_5:68;
then
card (rho .: (Funcs VAR ,(L . a))) in card W
by A21, CARD_2:3, ORDINAL1:22;
then
rho .: (Funcs VAR ,(L . a)) in W
by A18, CLASSES1:2;
then reconsider b =
sup (rho .: (Funcs VAR ,(L . a))) as
Ordinal of
W by Th28;
take
b
;
S3[a,b]
thus
S3[
a,
b]
;
verum
end;
A22:
for
a,
b1,
b2 being
Ordinal of
W st
S3[
a,
b1] &
S3[
a,
b2] holds
b1 = b2
;
consider si being
Ordinal-Sequence of
W such that A23:
for
a being
Ordinal of
W holds
S3[
a,
si . a]
from ZF_REFLE:sch 2(A22, A17);
deffunc H2(
Ordinal of
W,
Ordinal of
W)
-> Element of
W =
succ ((si . (succ $1)) \/ $2);
consider ksi being
Ordinal-Sequence of
W such that A24:
ksi . (0-element_of W) = si . (0-element_of W)
and A25:
for
a being
Ordinal of
W holds
ksi . (succ a) = H2(
a,
ksi . a)
and A26:
for
a being
Ordinal of
W st
a <> 0-element_of W &
a is
limit_ordinal holds
ksi . a = H1(
a,
ksi | a)
from ZF_REFLE:sch 3();
defpred S4[
Ordinal]
means si . $1
c= ksi . $1;
given phi being
Ordinal-Sequence of
W such that A27:
phi is
increasing
and A28:
phi is
continuous
and A29:
for
a being
Ordinal of
W st
phi . a = a &
{} <> a holds
for
f being
Function of
VAR ,
(L . a) holds
(
Union L,
(Union L) ! f |= the_scope_of H iff
L . a,
f |= the_scope_of H )
;
S1[H]
A30:
ksi is
increasing
A46:
0-element_of W = {}
by ORDINAL4:35;
A47:
ksi is
continuous
proof
let A be
Ordinal;
ORDINAL2:def 17 for b1 being set holds
( not A in proj1 ksi or A = {} or not A is limit_ordinal or not b1 = ksi . A or b1 is_limes_of ksi | A )let B be
Ordinal;
( not A in proj1 ksi or A = {} or not A is limit_ordinal or not B = ksi . A or B is_limes_of ksi | A )
assume that A48:
A in dom ksi
and A49:
A <> {}
and A50:
A is
limit_ordinal
and A51:
B = ksi . A
;
B is_limes_of ksi | A
A c= dom ksi
by A48, ORDINAL1:def 2;
then A52:
dom (ksi | A) = A
by RELAT_1:91;
reconsider a =
A as
Ordinal of
W by A48, ORDINAL1:def 10;
A53:
B =
union (ksi | a),
a
by A26, A46, A49, A50, A51
.=
Union (ksi | a)
by Th17
.=
union (rng (ksi | a))
by CARD_3:def 4
;
A54:
B c= sup (ksi | A)
A57:
ksi | A is
increasing
by A30, ORDINAL4:15;
A58:
sup (ksi | A) c= B
proof
let C be
Ordinal;
ORDINAL1:def 5 ( not C in sup (ksi | A) or C in B )
assume
C in sup (ksi | A)
;
C in B
then consider D being
Ordinal such that A59:
D in rng (ksi | A)
and A60:
C c= D
by ORDINAL2:29;
consider x being
set such that A61:
x in dom (ksi | A)
and A62:
D = (ksi | A) . x
by A59, FUNCT_1:def 5;
reconsider x =
x as
Ordinal by A61;
A63:
succ x in A
by A50, A52, A61, ORDINAL1:41;
then A64:
(ksi | A) . (succ x) in rng (ksi | A)
by A52, FUNCT_1:def 5;
x in succ x
by ORDINAL1:10;
then
D in (ksi | A) . (succ x)
by A52, A57, A62, A63, ORDINAL2:def 16;
then
D in B
by A53, A64, TARSKI:def 4;
hence
C in B
by A60, ORDINAL1:22;
verum
end;
sup (ksi | A) is_limes_of ksi | A
by A49, A50, A52, A57, ORDINAL4:8;
hence
B is_limes_of ksi | A
by A54, A58, XBOOLE_0:def 10;
verum
end;
A65:
for
a being
Ordinal of
W st
a <> 0-element_of W &
a is
limit_ordinal holds
si . a c= sup (si | a)
proof
let a be
Ordinal of
W;
( a <> 0-element_of W & a is limit_ordinal implies si . a c= sup (si | a) )
defpred S5[
set ]
means $1
in Free ('not' (the_scope_of H));
assume that A66:
a <> 0-element_of W
and A67:
a is
limit_ordinal
;
si . a c= sup (si | a)
A68:
si . a = sup (rho .: (Funcs VAR ,(L . a)))
by A23;
let A be
Ordinal;
ORDINAL1:def 5 ( not A in si . a or A in sup (si | a) )
assume
A in si . a
;
A in sup (si | a)
then consider B being
Ordinal such that A69:
B in rho .: (Funcs VAR ,(L . a))
and A70:
A c= B
by A68, ORDINAL2:29;
consider x being
set such that A71:
x in dom rho
and A72:
x in Funcs VAR ,
(L . a)
and A73:
B = rho . x
by A69, FUNCT_1:def 12;
reconsider h =
x as
Element of
Funcs VAR ,
(Union L) by A15, A71;
consider a1 being
Ordinal of
W such that A74:
a1 = rho . h
and A75:
ex
f being
Function of
VAR ,
(Union L) st
(
h = f & ( ex
m being
Element of
Union L st
(
m in L . a1 &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
a1 = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) )
and A76:
for
b being
Ordinal of
W st ex
f being
Function of
VAR ,
(Union L) st
(
h = f & ( ex
m being
Element of
Union L st
(
m in L . b &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
b = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) ) holds
a1 c= b
by A16;
consider f being
Function of
VAR ,
(Union L) such that A77:
h = f
and A78:
( ex
m being
Element of
Union L st
(
m in L . a1 &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
a1 = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) )
by A75;
defpred S6[
set ,
set ]
means for
a being
Ordinal of
W st
f . $1
in L . a holds
f . $2
in L . a;
A79:
now A80:
for
x,
y being
set holds
(
S6[
x,
y] or
S6[
y,
x] )
assume
Free ('not' (the_scope_of H)) <> {}
;
ex x being Ordinal of W st
( x in a & ( for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . x ) )then A83:
Free ('not' (the_scope_of H)) <> {}
;
A84:
(
L . a = Union (L | a) &
Union (L | a) = union (rng (L | a)) )
by A3, A46, A66, A67, CARD_3:def 4;
A85:
for
x,
y,
z being
set st
S6[
x,
y] &
S6[
y,
z] holds
S6[
x,
z]
;
consider z being
set such that A86:
(
z in Free ('not' (the_scope_of H)) & ( for
y being
set st
y in Free ('not' (the_scope_of H)) holds
S6[
z,
y] ) )
from CARD_3:sch 3(A83, A80, A85);
reconsider z =
z as
Variable by A86;
A87:
dom (L | a) c= a
by RELAT_1:87;
A88:
ex
s being
Function st
(
f = s &
dom s = VAR &
rng s c= L . a )
by A72, A77, FUNCT_2:def 2;
then
f . z in rng f
by FUNCT_1:def 5;
then consider X being
set such that A89:
f . z in X
and A90:
X in rng (L | a)
by A88, A84, TARSKI:def 4;
consider x being
set such that A91:
x in dom (L | a)
and A92:
X = (L | a) . x
by A90, FUNCT_1:def 5;
A93:
(L | a) . x = L . x
by A91, FUNCT_1:70;
reconsider x =
x as
Ordinal by A91;
a in On W
by ORDINAL1:def 10;
then
x in On W
by A91, A87, ORDINAL1:19;
then reconsider x =
x as
Ordinal of
W by ORDINAL1:def 10;
take x =
x;
( x in a & ( for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . x ) )thus
x in a
by A91, A87;
for y being Variable st y in Free ('not' (the_scope_of H)) holds
f . y in L . xlet y be
Variable;
( y in Free ('not' (the_scope_of H)) implies f . y in L . x )assume
y in Free ('not' (the_scope_of H))
;
f . y in L . xhence
f . y in L . x
by A86, A89, A92, A93;
verum end;
then consider c being
Ordinal of
W such that A95:
c in a
and A96:
for
x1 being
Variable st
x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . c
by A79;
A97:
si . c = sup (rho .: (Funcs VAR ,(L . c)))
by A23;
(
c in dom si &
dom (si | a) = (dom si) /\ a )
by ORDINAL4:36, RELAT_1:90;
then A98:
c in dom (si | a)
by A95, XBOOLE_0:def 4;
si . c = (si | a) . c
by A95, FUNCT_1:72;
then
si . c in rng (si | a)
by A98, FUNCT_1:def 5;
then A99:
si . c in sup (si | a)
by ORDINAL2:27;
deffunc H3(
set )
-> set =
f . $1;
consider e being
Element of
L . c;
deffunc H4(
set )
-> Element of
L . c =
e;
consider v being
Function such that A100:
(
dom v = VAR & ( for
x being
set st
x in VAR holds
( (
S5[
x] implies
v . x = H3(
x) ) & ( not
S5[
x] implies
v . x = H4(
x) ) ) ) )
from PARTFUN1:sch 1();
A101:
rng v c= L . c
then reconsider v =
v as
Function of
VAR ,
(L . c) by A100, FUNCT_2:def 1, RELSET_1:11;
A104:
v in Funcs VAR ,
(L . c)
by A100, A101, FUNCT_2:def 2;
Funcs VAR ,
(L . c) c= Funcs VAR ,
(Union L)
by Th24, FUNCT_5:63;
then reconsider v9 =
v as
Element of
Funcs VAR ,
(Union L) by A104;
consider a2 being
Ordinal of
W such that A105:
a2 = rho . v9
and A106:
ex
f being
Function of
VAR ,
(Union L) st
(
v9 = f & ( ex
m being
Element of
Union L st
(
m in L . a2 &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
a2 = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) )
and A107:
for
b being
Ordinal of
W st ex
f being
Function of
VAR ,
(Union L) st
(
v9 = f & ( ex
m being
Element of
Union L st
(
m in L . b &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
b = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) ) holds
a2 c= b
by A16;
consider f9 being
Function of
VAR ,
(Union L) such that A108:
v9 = f9
and A109:
( ex
m being
Element of
Union L st
(
m in L . a2 &
Union L,
f9 / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
a2 = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f9 / (bound_in H),
m |= 'not' (the_scope_of H) ) ) )
by A106;
A110:
v = (Union L) ! v
by Th24, ZF_LANG1:def 2;
A111:
now given m being
Element of
Union L such that A112:
m in L . a1
and A113:
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H)
;
a1 = a2A114:
now let x1 be
Variable;
( x1 in Free ('not' (the_scope_of H)) implies (f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1 )A115:
(f / (bound_in H),m) . (bound_in H) = m
by FUNCT_7:130;
A116:
(
x1 <> bound_in H implies (
(f / (bound_in H),m) . x1 = f . x1 &
(((Union L) ! v) / (bound_in H),m) . x1 = ((Union L) ! v) . x1 ) )
by FUNCT_7:34;
assume
x1 in Free ('not' (the_scope_of H))
;
(f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1hence
(f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1
by A100, A110, A115, A116, FUNCT_7:130;
verum end; then
Union L,
((Union L) ! v) / (bound_in H),
m |= 'not' (the_scope_of H)
by A113, ZF_LANG1:84;
then consider m9 being
Element of
Union L such that A117:
(
m9 in L . a2 &
Union L,
f9 / (bound_in H),
m9 |= 'not' (the_scope_of H) )
by A110, A108, A109;
now let x1 be
Variable;
( x1 in Free ('not' (the_scope_of H)) implies (f / (bound_in H),m9) . x1 = (f9 / (bound_in H),m9) . x1 )A118:
(f / (bound_in H),m9) . (bound_in H) = m9
by FUNCT_7:130;
A119:
(
x1 <> bound_in H implies (
(f / (bound_in H),m9) . x1 = f . x1 &
(((Union L) ! v) / (bound_in H),m9) . x1 = ((Union L) ! v) . x1 ) )
by FUNCT_7:34;
assume
x1 in Free ('not' (the_scope_of H))
;
(f / (bound_in H),m9) . x1 = (f9 / (bound_in H),m9) . x1hence
(f / (bound_in H),m9) . x1 = (f9 / (bound_in H),m9) . x1
by A100, A110, A108, A118, A119, FUNCT_7:130;
verum end; then A120:
a1 c= a2
by A76, A77, A117, ZF_LANG1:84;
a2 c= a1
by A110, A107, A112, A113, A114, ZF_LANG1:84;
hence
a1 = a2
by A120, XBOOLE_0:def 10;
verum end;
now assume A121:
for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H)
;
a1 = a2now let m be
Element of
Union L;
not Union L,((Union L) ! v) / (bound_in H),m |= 'not' (the_scope_of H)now let x1 be
Variable;
( x1 in Free ('not' (the_scope_of H)) implies (f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1 )A122:
(f / (bound_in H),m) . (bound_in H) = m
by FUNCT_7:130;
A123:
(
x1 <> bound_in H implies (
(f / (bound_in H),m) . x1 = f . x1 &
(((Union L) ! v) / (bound_in H),m) . x1 = ((Union L) ! v) . x1 ) )
by FUNCT_7:34;
assume
x1 in Free ('not' (the_scope_of H))
;
(f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1hence
(f / (bound_in H),m) . x1 = (((Union L) ! v) / (bound_in H),m) . x1
by A100, A110, A122, A123, FUNCT_7:130;
verum end; hence
not
Union L,
((Union L) ! v) / (bound_in H),
m |= 'not' (the_scope_of H)
by A121, ZF_LANG1:84;
verum end; hence
a1 = a2
by A78, A110, A108, A109, A121;
verum end;
then
B in rho .: (Funcs VAR ,(L . c))
by A15, A73, A74, A75, A77, A104, A105, A111, FUNCT_1:def 12;
then
B in si . c
by A97, ORDINAL2:27;
then
B in sup (si | a)
by A99, ORDINAL1:19;
hence
A in sup (si | a)
by A70, ORDINAL1:22;
verum
end;
A124:
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
S4[
b] ) holds
S4[
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
S4[b] ) implies S4[a] )
assume that A125:
(
a <> 0-element_of W &
a is
limit_ordinal )
and A126:
for
b being
Ordinal of
W st
b in a holds
si . b c= ksi . b
;
S4[a]
thus
si . a c= ksi . a
verumproof
A127:
si . a c= sup (si | a)
by A65, A125;
let A be
Ordinal;
ORDINAL1:def 5 ( not A in si . a or A in ksi . a )
assume
A in si . a
;
A in ksi . a
then consider B being
Ordinal such that A128:
B in rng (si | a)
and A129:
A c= B
by A127, ORDINAL2:29;
consider x being
set such that A130:
x in dom (si | a)
and A131:
B = (si | a) . x
by A128, FUNCT_1:def 5;
A132:
dom (si | a) c= a
by RELAT_1:87;
reconsider x =
x as
Ordinal by A130;
A133:
a in On W
by ORDINAL1:def 10;
x in On W
by A130;
then reconsider x =
x as
Ordinal of
W by ORDINAL1:def 10;
A134:
si . x = B
by A130, A131, FUNCT_1:70;
A135:
si . x c= ksi . x
by A126, A130, A132;
dom ksi = On W
by FUNCT_2:def 1;
then
ksi . x in ksi . a
by A30, A130, A132, A133, ORDINAL2:def 16;
hence
A in ksi . a
by A129, A134, A135, ORDINAL1:22, XBOOLE_1:1;
verum
end;
end;
A136:
for
a being
Ordinal of
W st
S4[
a] holds
S4[
succ a]
A137:
S4[
0-element_of W]
by A24;
A138:
for
a being
Ordinal of
W holds
S4[
a]
from ZF_REFLE:sch 4(A137, A136, A124);
A139:
now assume
bound_in H in Free (the_scope_of H)
;
S1[H]thus
S1[
H]
verumproof
take gamma =
phi * ksi;
( gamma is increasing & gamma is continuous & ( for a being Ordinal of W st gamma . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
ex
f being
Ordinal-Sequence st
(
f = phi * ksi &
f is
increasing )
by A27, A30, ORDINAL4:13;
hence
(
gamma is
increasing &
gamma is
continuous )
by A28, A30, A47, ORDINAL4:17;
for a being Ordinal of W st gamma . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be
Ordinal of
W;
( gamma . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume that A140:
gamma . a = a
and A141:
{} <> a
;
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be
Function of
VAR ,
(L . a);
( Union L,(Union L) ! f |= H iff L . a,f |= H )
a in dom gamma
by ORDINAL4:36;
then A142:
phi . (ksi . a) = gamma . a
by FUNCT_1:22;
a in dom ksi
by ORDINAL4:36;
then A143:
a c= ksi . a
by A30, ORDINAL4:10;
ksi . a in dom phi
by ORDINAL4:36;
then A144:
ksi . a c= phi . (ksi . a)
by A27, ORDINAL4:10;
then A145:
ksi . a = a
by A140, A143, A142, XBOOLE_0:def 10;
A146:
phi . a = a
by A140, A144, A143, A142, XBOOLE_0:def 10;
thus
(
Union L,
(Union L) ! f |= H implies
L . a,
f |= H )
( L . a,f |= H implies Union L,(Union L) ! f |= H )
assume that A149:
L . a,
f |= H
and A150:
not
Union L,
(Union L) ! f |= H
;
contradiction
consider m being
Element of
Union L such that A151:
not
Union L,
((Union L) ! f) / (bound_in H),
m |= the_scope_of H
by A7, A150, ZF_LANG1:80;
A152:
si . a c= ksi . a
by A138;
A153:
si . a = sup (rho .: (Funcs VAR ,(L . a)))
by A23;
reconsider h =
(Union L) ! f as
Element of
Funcs VAR ,
(Union L) by FUNCT_2:11;
consider a1 being
Ordinal of
W such that A154:
a1 = rho . h
and A155:
ex
f being
Function of
VAR ,
(Union L) st
(
h = f & ( ex
m being
Element of
Union L st
(
m in L . a1 &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
a1 = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) )
and
for
b being
Ordinal of
W st ex
f being
Function of
VAR ,
(Union L) st
(
h = f & ( ex
m being
Element of
Union L st
(
m in L . b &
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) or (
b = 0-element_of W & ( for
m being
Element of
Union L holds not
Union L,
f / (bound_in H),
m |= 'not' (the_scope_of H) ) ) ) ) holds
a1 c= b
by A16;
A156:
(Union L) ! f = f
by Th24, ZF_LANG1:def 2;
Union L,
((Union L) ! f) / (bound_in H),
m |= 'not' (the_scope_of H)
by A151, ZF_MODEL:14;
then consider m being
Element of
Union L such that A157:
m in L . a1
and A158:
Union L,
((Union L) ! f) / (bound_in H),
m |= 'not' (the_scope_of H)
by A155;
f in Funcs VAR ,
(L . a)
by FUNCT_2:11;
then
a1 in rho .: (Funcs VAR ,(L . a))
by A15, A154, A156, FUNCT_1:def 12;
then
a1 in si . a
by A153, ORDINAL2:27;
then
L . a1 c= L . a
by A2, A145, A152;
then reconsider m9 =
m as
Element of
L . a by A157;
((Union L) ! f) / (bound_in H),
m = (Union L) ! (f / (bound_in H),m9)
by A156, Th24, ZF_LANG1:def 2;
then
not
Union L,
(Union L) ! (f / (bound_in H),m9) |= the_scope_of H
by A158, ZF_MODEL:14;
then
not
L . a,
f / (bound_in H),
m9 |= the_scope_of H
by A29, A141, A146;
hence
contradiction
by A7, A149, ZF_LANG1:80;
verum
(
dom (((Union L) ! f) / (bound_in H),m) = VAR &
rng (((Union L) ! f) / (bound_in H),m) c= L . a )
then reconsider g =
((Union L) ! f) / (bound_in H),
m as
Function of
VAR ,
(L . a) by FUNCT_2:def 1, RELSET_1:11;
end; end;
now assume A161:
not
bound_in H in Free (the_scope_of H)
;
S1[H]thus
S1[
H]
verumproof
take
phi
;
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus
(
phi is
increasing &
phi is
continuous )
by A27, A28;
for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be
Ordinal of
W;
( phi . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume A162:
(
phi . a = a &
{} <> a )
;
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be
Function of
VAR ,
(L . a);
( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus
(
Union L,
(Union L) ! f |= H implies
L . a,
f |= H )
( L . a,f |= H implies Union L,(Union L) ! f |= H )proof
A163:
for
k being
Variable st
((Union L) ! f) . k <> ((Union L) ! f) . k holds
bound_in H = k
;
assume
Union L,
(Union L) ! f |= H
;
L . a,f |= H
then
Union L,
(Union L) ! f |= the_scope_of H
by A7, A163, ZF_MODEL:16;
then
L . a,
f |= the_scope_of H
by A29, A162;
hence
L . a,
f |= H
by A7, A161, ZFMODEL1:10;
verum
end;
A164:
for
k being
Variable st
f . k <> f . k holds
bound_in H = k
;
assume
L . a,
f |= H
;
Union L,(Union L) ! f |= H
then
L . a,
f |= the_scope_of H
by A7, A164, ZF_MODEL:16;
then
Union L,
(Union L) ! f |= the_scope_of H
by A29, A162;
hence
Union L,
(Union L) ! f |= H
by A7, A161, ZFMODEL1:10;
verum
end; end;
hence
S1[
H]
by A139;
verum
end;
A165:
for H being ZF-formula st H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] holds
S1[H]
proof
let H be
ZF-formula;
( H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] implies S1[H] )
assume
H is
conjunctive
;
( not S1[ the_left_argument_of H] or not S1[ the_right_argument_of H] or S1[H] )
then A166:
H = (the_left_argument_of H) '&' (the_right_argument_of H)
by ZF_LANG:58;
given fi1 being
Ordinal-Sequence of
W such that A167:
fi1 is
increasing
and A168:
fi1 is
continuous
and A169:
for
a being
Ordinal of
W st
fi1 . a = a &
{} <> a holds
for
f being
Function of
VAR ,
(L . a) holds
(
Union L,
(Union L) ! f |= the_left_argument_of H iff
L . a,
f |= the_left_argument_of H )
;
( not S1[ the_right_argument_of H] or S1[H] )
given fi2 being
Ordinal-Sequence of
W such that A170:
fi2 is
increasing
and A171:
fi2 is
continuous
and A172:
for
a being
Ordinal of
W st
fi2 . a = a &
{} <> a holds
for
f being
Function of
VAR ,
(L . a) holds
(
Union L,
(Union L) ! f |= the_right_argument_of H iff
L . a,
f |= the_right_argument_of H )
;
S1[H]
take phi =
fi2 * fi1;
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
ex
fi being
Ordinal-Sequence st
(
fi = fi2 * fi1 &
fi is
increasing )
by A167, A170, ORDINAL4:13;
hence
(
phi is
increasing &
phi is
continuous )
by A167, A168, A171, ORDINAL4:17;
for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be
Ordinal of
W;
( phi . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume that A173:
phi . a = a
and A174:
{} <> a
;
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
a in dom fi1
by ORDINAL4:36;
then A175:
a c= fi1 . a
by A167, ORDINAL4:10;
let f be
Function of
VAR ,
(L . a);
( Union L,(Union L) ! f |= H iff L . a,f |= H )
A176:
a in dom phi
by ORDINAL4:36;
A177:
a in dom fi2
by ORDINAL4:36;
then A181:
fi2 . a = a
by A173, A176, FUNCT_1:22;
thus
(
Union L,
(Union L) ! f |= H implies
L . a,
f |= H )
( L . a,f |= H implies Union L,(Union L) ! f |= H )proof
assume A182:
Union L,
(Union L) ! f |= H
;
L . a,f |= H
then
Union L,
(Union L) ! f |= the_right_argument_of H
by A166, ZF_MODEL:15;
then A183:
L . a,
f |= the_right_argument_of H
by A172, A174, A181;
Union L,
(Union L) ! f |= the_left_argument_of H
by A166, A182, ZF_MODEL:15;
then
L . a,
f |= the_left_argument_of H
by A169, A174, A178;
hence
L . a,
f |= H
by A166, A183, ZF_MODEL:15;
verum
end;
assume A184:
L . a,
f |= H
;
Union L,(Union L) ! f |= H
then
L . a,
f |= the_right_argument_of H
by A166, ZF_MODEL:15;
then A185:
Union L,
(Union L) ! f |= the_right_argument_of H
by A172, A174, A181;
L . a,
f |= the_left_argument_of H
by A166, A184, ZF_MODEL:15;
then
Union L,
(Union L) ! f |= the_left_argument_of H
by A169, A174, A178;
hence
Union L,
(Union L) ! f |= H
by A166, A185, ZF_MODEL:15;
verum
end;
A186:
for H being ZF-formula st H is atomic holds
S1[H]
proof
A187:
dom (id (On W)) = On W
by RELAT_1:71;
then reconsider phi =
id (On W) as
T-Sequence by ORDINAL1:def 7;
A188:
rng (id (On W)) = On W
by RELAT_1:71;
then reconsider phi =
phi as
Ordinal-Sequence by ORDINAL2:def 8;
reconsider phi =
phi as
Ordinal-Sequence of
W by A187, A188, FUNCT_2:def 1, RELSET_1:11;
let H be
ZF-formula;
( H is atomic implies S1[H] )
assume A189:
(
H is
being_equality or
H is
being_membership )
;
ZF_LANG:def 15 S1[H]
take
phi
;
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus A190:
phi is
increasing
( phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus
phi is
continuous
for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )proof
let A be
Ordinal;
ORDINAL2:def 17 for b1 being set holds
( not A in proj1 phi or A = {} or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A )let B be
Ordinal;
( not A in proj1 phi or A = {} or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )
assume that A192:
A in dom phi
and A193:
(
A <> {} &
A is
limit_ordinal )
and A194:
B = phi . A
;
B is_limes_of phi | A
A195:
A c= dom phi
by A192, ORDINAL1:def 2;
phi | A =
phi * (id A)
by RELAT_1:94
.=
id ((dom phi) /\ A)
by A187, FUNCT_1:43
.=
id A
by A195, XBOOLE_1:28
;
then A196:
rng (phi | A) = A
by RELAT_1:71;
phi . A = A
by A192, FUNCT_1:35;
then A197:
sup (phi | A) = B
by A194, A196, ORDINAL2:26;
A198:
phi | A is
increasing
by A190, ORDINAL4:15;
dom (phi | A) = A
by A195, RELAT_1:91;
hence
B is_limes_of phi | A
by A193, A197, A198, ORDINAL4:8;
verum
end;
let a be
Ordinal of
W;
( phi . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume that
phi . a = a
and
{} <> a
;
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be
Function of
VAR ,
(L . a);
( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus
(
Union L,
(Union L) ! f |= H implies
L . a,
f |= H )
( L . a,f |= H implies Union L,(Union L) ! f |= H )
assume A204:
L . a,
f |= H
;
Union L,(Union L) ! f |= H
A205:
(Union L) ! f = f
by Th24, ZF_LANG1:def 2;
hence
Union L,
(Union L) ! f |= H
by A189, A206;
verum
end;
A209:
for H being ZF-formula st H is negative & S1[ the_argument_of H] holds
S1[H]
proof
let H be
ZF-formula;
( H is negative & S1[ the_argument_of H] implies S1[H] )
assume
H is
negative
;
( not S1[ the_argument_of H] or S1[H] )
then A210:
H = 'not' (the_argument_of H)
by ZF_LANG:def 30;
given phi being
Ordinal-Sequence of
W such that A211:
(
phi is
increasing &
phi is
continuous )
and A212:
for
a being
Ordinal of
W st
phi . a = a &
{} <> a holds
for
f being
Function of
VAR ,
(L . a) holds
(
Union L,
(Union L) ! f |= the_argument_of H iff
L . a,
f |= the_argument_of H )
;
S1[H]
take
phi
;
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
thus
(
phi is
increasing &
phi is
continuous )
by A211;
for a being Ordinal of W st phi . a = a & {} <> a holds
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let a be
Ordinal of
W;
( phi . a = a & {} <> a implies for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) )
assume A213:
(
phi . a = a &
{} <> a )
;
for f being Function of VAR ,(L . a) holds
( Union L,(Union L) ! f |= H iff L . a,f |= H )
let f be
Function of
VAR ,
(L . a);
( Union L,(Union L) ! f |= H iff L . a,f |= H )
thus
(
Union L,
(Union L) ! f |= H implies
L . a,
f |= H )
( L . a,f |= H implies Union L,(Union L) ! f |= H )
assume
L . a,
f |= H
;
Union L,(Union L) ! f |= H
then
not
L . a,
f |= the_argument_of H
by A210, ZF_MODEL:14;
then
not
Union L,
(Union L) ! f |= the_argument_of H
by A212, A213;
hence
Union L,
(Union L) ! f |= H
by A210, ZF_MODEL:14;
verum
end;
thus
for H being ZF-formula holds S1[H]
from ZF_LANG:sch 1(A186, A209, A165, A6); verum