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 Def2;
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:44;
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 ex a being Ordinal of W st S2[h,a]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
object such that A13:
x in dom L
and A14:
X = L . x
by A12, FUNCT_1:def 3;
reconsider x =
x as
Ordinal by A13;
reconsider b =
x as
Ordinal of
W by A5, A13, ORDINAL1:def 9;
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
object ;
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
object such that
h in dom rho
and A19:
h in Funcs (
VAR,
(L . a))
and A20:
x = rho . h
by FUNCT_1:def 6;
Funcs (
VAR,
(L . a))
c= Funcs (
VAR,
(Union L))
by Th16, FUNCT_5:56;
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:61;
then A21:
card (Funcs (omega,(L . a))) in card W
by CLASSES2:1;
(
card VAR = card omega &
card (L . a) = card (L . a) )
by Th17, CARD_1:5;
then
card (Funcs (VAR,(L . a))) = card (Funcs (omega,(L . a)))
by FUNCT_5:61;
then
card (rho .: (Funcs (VAR,(L . a)))) in card W
by A21, CARD_1:67, ORDINAL1:12;
then
rho .: (Funcs (VAR,(L . a))) in W
by A18, CLASSES1:1;
then reconsider b =
sup (rho .: (Funcs (VAR,(L . a)))) as
Ordinal of
W by Th19;
take
b
;
S3[a,b]
thus
S3[
a,
b]
;
verum
end;
consider si being
Ordinal-Sequence of
W such that A22:
for
a being
Ordinal of
W holds
S3[
a,
si . a]
from ZF_REFLE:sch 2(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 A23:
ksi . (0-element_of W) = si . (0-element_of W)
and A24:
for
a being
Ordinal of
W holds
ksi . (succ a) = H2(
a,
ksi . a)
and A25:
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 A26:
phi is
increasing
and A27:
phi is
continuous
and 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 |= the_scope_of H iff
L . a,
f |= the_scope_of H )
;
S1[H]
A29:
ksi is
increasing
A45:
0-element_of W = {}
by ORDINAL4:33;
A46:
ksi is
continuous
proof
let A be
Ordinal;
ORDINAL2:def 13 for b1 being set holds
( not A in dom ksi or A = 0 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 dom ksi or A = 0 or not A is limit_ordinal or not B = ksi . A or B is_limes_of ksi | A )
assume that A47:
A in dom ksi
and A48:
A <> 0
and A49:
A is
limit_ordinal
and A50:
B = ksi . A
;
B is_limes_of ksi | A
A c= dom ksi
by A47, ORDINAL1:def 2;
then A51:
dom (ksi | A) = A
by RELAT_1:62;
reconsider a =
A as
Ordinal of
W by A47, ORDINAL1:def 9;
A52:
B =
union (
(ksi | a),
a)
by A25, A45, A48, A49, A50
.=
Union (ksi | a)
by Th14
.=
union (rng (ksi | a))
by CARD_3:def 4
;
A53:
B c= sup (ksi | A)
A56:
ksi | A is
increasing
by A29, ORDINAL4:15;
A57:
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 A58:
D in rng (ksi | A)
and A59:
C c= D
by ORDINAL2:21;
consider x being
object such that A60:
x in dom (ksi | A)
and A61:
D = (ksi | A) . x
by A58, FUNCT_1:def 3;
reconsider x =
x as
Ordinal by A60;
A62:
succ x in A
by A49, A60, ORDINAL1:28;
then A63:
(ksi | A) . (succ x) in rng (ksi | A)
by A51, FUNCT_1:def 3;
x in succ x
by ORDINAL1:6;
then
D in (ksi | A) . (succ x)
by A51, A56, A61, A62;
then
D in B
by A52, A63, TARSKI:def 4;
hence
C in B
by A59, ORDINAL1:12;
verum
end;
sup (ksi | A) is_limes_of ksi | A
by A48, A49, A51, A56, ORDINAL4:8;
hence
B is_limes_of ksi | A
by A53, A57, XBOOLE_0:def 10;
verum
end;
A64:
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[
object ]
means $1
in Free ('not' (the_scope_of H));
assume that A65:
a <> 0-element_of W
and A66:
a is
limit_ordinal
;
si . a c= sup (si | a)
A67:
si . a = sup (rho .: (Funcs (VAR,(L . a))))
by A22;
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 A68:
B in rho .: (Funcs (VAR,(L . a)))
and A69:
A c= B
by A67, ORDINAL2:21;
consider x being
object such that A70:
x in dom rho
and A71:
x in Funcs (
VAR,
(L . a))
and A72:
B = rho . x
by A68, FUNCT_1:def 6;
reconsider h =
x as
Element of
Funcs (
VAR,
(Union L))
by A15, A70;
consider a1 being
Ordinal of
W such that A73:
a1 = rho . h
and A74:
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 A75:
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 A76:
h = f
and A77:
( 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 A74;
defpred S6[
object ,
object ]
means for
a being
Ordinal of
W st
f . $1
in L . a holds
f . $2
in L . a;
A78:
now ( Free ('not' (the_scope_of H)) <> {} implies 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 ) ) )A79:
for
x,
y being
object 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 A82:
Free ('not' (the_scope_of H)) <> {}
;
A83:
(
L . a = Union (L | a) &
Union (L | a) = union (rng (L | a)) )
by A3, A45, A65, A66, CARD_3:def 4;
A84:
for
x,
y,
z being
object st
S6[
x,
y] &
S6[
y,
z] holds
S6[
x,
z]
;
consider z being
object such that A85:
(
z in Free ('not' (the_scope_of H)) & ( for
y being
object st
y in Free ('not' (the_scope_of H)) holds
S6[
z,
y] ) )
from CARD_2:sch 2(A82, A79, A84);
reconsider z =
z as
Variable by A85;
A86:
dom (L | a) c= a
by RELAT_1:58;
A87:
ex
s being
Function st
(
f = s &
dom s = VAR &
rng s c= L . a )
by A71, A76, FUNCT_2:def 2;
then
f . z in rng f
by FUNCT_1:def 3;
then consider X being
set such that A88:
f . z in X
and A89:
X in rng (L | a)
by A87, A83, TARSKI:def 4;
consider x being
object such that A90:
x in dom (L | a)
and A91:
X = (L | a) . x
by A89, FUNCT_1:def 3;
A92:
(L | a) . x = L . x
by A90, FUNCT_1:47;
reconsider x =
x as
Ordinal by A90;
a in On W
by ORDINAL1:def 9;
then
x in On W
by A90, A86, ORDINAL1:10;
then reconsider x =
x as
Ordinal of
W by ORDINAL1:def 9;
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 A90, A86;
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 A85, A88, A91, A92;
verum end;
then consider c being
Ordinal of
W such that A94:
c in a
and A95:
for
x1 being
Variable st
x1 in Free ('not' (the_scope_of H)) holds
f . x1 in L . c
by A78;
A96:
si . c = sup (rho .: (Funcs (VAR,(L . c))))
by A22;
(
c in dom si &
dom (si | a) = (dom si) /\ a )
by ORDINAL4:34, RELAT_1:61;
then A97:
c in dom (si | a)
by A94, XBOOLE_0:def 4;
si . c = (si | a) . c
by A94, FUNCT_1:49;
then
si . c in rng (si | a)
by A97, FUNCT_1:def 3;
then A98:
si . c in sup (si | a)
by ORDINAL2:19;
deffunc H3(
object )
-> set =
f . $1;
set e = the
Element of
L . c;
deffunc H4(
object )
-> Element of
L . c = the
Element of
L . c;
consider v being
Function such that A99:
(
dom v = VAR & ( for
x being
object st
x in VAR holds
( (
S5[
x] implies
v . x = H3(
x) ) & ( not
S5[
x] implies
v . x = H4(
x) ) ) ) )
from PARTFUN1:sch 1();
A100:
rng v c= L . c
then reconsider v =
v as
Function of
VAR,
(L . c) by A99, FUNCT_2:def 1, RELSET_1:4;
A103:
v in Funcs (
VAR,
(L . c))
by A99, A100, FUNCT_2:def 2;
Funcs (
VAR,
(L . c))
c= Funcs (
VAR,
(Union L))
by Th16, FUNCT_5:56;
then reconsider v9 =
v as
Element of
Funcs (
VAR,
(Union L))
by A103;
consider a2 being
Ordinal of
W such that A104:
a2 = rho . v9
and A105:
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 A106:
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 A107:
v9 = f9
and A108:
( 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 A105;
A109:
v = (Union L) ! v
by Th16, ZF_LANG1:def 1;
A110:
now ( ex m being Element of Union L st
( m in L . a1 & Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) implies a1 = a2 )given m being
Element of
Union L such that A111:
m in L . a1
and A112:
Union L,
f / (
(bound_in H),
m)
|= 'not' (the_scope_of H)
;
a1 = a2A113:
now for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
(f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1let 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 )A114:
(f / ((bound_in H),m)) . (bound_in H) = m
by FUNCT_7:128;
A115:
(
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:32;
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 A99, A109, A114, A115, FUNCT_7:128;
verum end; then
Union L,
((Union L) ! v) / (
(bound_in H),
m)
|= 'not' (the_scope_of H)
by A112, ZF_LANG1:75;
then consider m9 being
Element of
Union L such that A116:
(
m9 in L . a2 &
Union L,
f9 / (
(bound_in H),
m9)
|= 'not' (the_scope_of H) )
by A109, A107, A108;
now for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
(f / ((bound_in H),m9)) . x1 = (f9 / ((bound_in H),m9)) . x1let x1 be
Variable;
( x1 in Free ('not' (the_scope_of H)) implies (f / ((bound_in H),m9)) . x1 = (f9 / ((bound_in H),m9)) . x1 )A117:
(f / ((bound_in H),m9)) . (bound_in H) = m9
by FUNCT_7:128;
A118:
(
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:32;
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 A99, A109, A107, A117, A118, FUNCT_7:128;
verum end; then A119:
a1 c= a2
by A75, A76, A116, ZF_LANG1:75;
a2 c= a1
by A109, A106, A111, A112, A113, ZF_LANG1:75;
hence
a1 = a2
by A119;
verum end;
now ( ( for m being Element of Union L holds not Union L,f / ((bound_in H),m) |= 'not' (the_scope_of H) ) implies a1 = a2 )assume A120:
for
m being
Element of
Union L holds not
Union L,
f / (
(bound_in H),
m)
|= 'not' (the_scope_of H)
;
a1 = a2now for m being Element of Union L holds not Union L,((Union L) ! v) / ((bound_in H),m) |= 'not' (the_scope_of H)let m be
Element of
Union L;
not Union L,((Union L) ! v) / ((bound_in H),m) |= 'not' (the_scope_of H)now for x1 being Variable st x1 in Free ('not' (the_scope_of H)) holds
(f / ((bound_in H),m)) . x1 = (((Union L) ! v) / ((bound_in H),m)) . x1let 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 )A121:
(f / ((bound_in H),m)) . (bound_in H) = m
by FUNCT_7:128;
A122:
(
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:32;
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 A99, A109, A121, A122, FUNCT_7:128;
verum end; hence
not
Union L,
((Union L) ! v) / (
(bound_in H),
m)
|= 'not' (the_scope_of H)
by A120, ZF_LANG1:75;
verum end; hence
a1 = a2
by A77, A109, A107, A108, A120;
verum end;
then
B in rho .: (Funcs (VAR,(L . c)))
by A15, A72, A73, A74, A76, A103, A104, A110, FUNCT_1:def 6;
then
B in si . c
by A96, ORDINAL2:19;
then
B in sup (si | a)
by A98, ORDINAL1:10;
hence
A in sup (si | a)
by A69, ORDINAL1:12;
verum
end;
A123:
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 A124:
(
a <> 0-element_of W &
a is
limit_ordinal )
and A125:
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
A126:
si . a c= sup (si | a)
by A64, A124;
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 A127:
B in rng (si | a)
and A128:
A c= B
by A126, ORDINAL2:21;
consider x being
object such that A129:
x in dom (si | a)
and A130:
B = (si | a) . x
by A127, FUNCT_1:def 3;
reconsider x =
x as
Ordinal by A129;
A131:
a in On W
by ORDINAL1:def 9;
x in dom si
by A129, RELAT_1:57;
then
x in On W
;
then reconsider x =
x as
Ordinal of
W by ORDINAL1:def 9;
A132:
si . x = B
by A129, A130, FUNCT_1:47;
A133:
si . x c= ksi . x
by A125, A129;
dom ksi = On W
by FUNCT_2:def 1;
then
ksi . x in ksi . a
by A29, A129, A131;
hence
A in ksi . a
by A128, A132, A133, ORDINAL1:12, XBOOLE_1:1;
verum
end;
end;
A134:
for
a being
Ordinal of
W st
S4[
a] holds
S4[
succ a]
A135:
S4[
0-element_of W]
by A23;
A136:
for
a being
Ordinal of
W holds
S4[
a]
from ZF_REFLE:sch 4(A135, A134, A123);
A137:
now ( bound_in H in Free (the_scope_of H) implies S1[H] )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 A26, A29, ORDINAL4:13;
hence
(
gamma is
increasing &
gamma is
continuous )
by A27, A29, A46, 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 A138:
gamma . a = a
and A139:
{} <> 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:34;
then A140:
phi . (ksi . a) = gamma . a
by FUNCT_1:12;
a in dom ksi
by ORDINAL4:34;
then A141:
a c= ksi . a
by A29, ORDINAL4:10;
ksi . a in dom phi
by ORDINAL4:34;
then A142:
ksi . a c= phi . (ksi . a)
by A26, ORDINAL4:10;
then A143:
ksi . a = a
by A138, A141, A140;
A144:
phi . a = a
by A138, A142, A141, A140, 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 A147:
L . a,
f |= H
and A148:
not
Union L,
(Union L) ! f |= H
;
contradiction
consider m being
Element of
Union L such that A149:
not
Union L,
((Union L) ! f) / (
(bound_in H),
m)
|= the_scope_of H
by A7, A148, ZF_LANG1:71;
A150:
si . a c= ksi . a
by A136;
A151:
si . a = sup (rho .: (Funcs (VAR,(L . a))))
by A22;
reconsider h =
(Union L) ! f as
Element of
Funcs (
VAR,
(Union L))
by FUNCT_2:8;
consider a1 being
Ordinal of
W such that A152:
a1 = rho . h
and A153:
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;
A154:
(Union L) ! f = f
by Th16, ZF_LANG1:def 1;
Union L,
((Union L) ! f) / (
(bound_in H),
m)
|= 'not' (the_scope_of H)
by A149, ZF_MODEL:14;
then consider m being
Element of
Union L such that A155:
m in L . a1
and A156:
Union L,
((Union L) ! f) / (
(bound_in H),
m)
|= 'not' (the_scope_of H)
by A153;
f in Funcs (
VAR,
(L . a))
by FUNCT_2:8;
then
a1 in rho .: (Funcs (VAR,(L . a)))
by A15, A152, A154, FUNCT_1:def 6;
then
a1 in si . a
by A151, ORDINAL2:19;
then
L . a1 c= L . a
by A2, A143, A150;
then reconsider m9 =
m as
Element of
L . a by A155;
((Union L) ! f) / (
(bound_in H),
m)
= (Union L) ! (f / ((bound_in H),m9))
by A154, Th16, ZF_LANG1:def 1;
then
not
Union L,
(Union L) ! (f / ((bound_in H),m9)) |= the_scope_of H
by A156, ZF_MODEL:14;
then
not
L . a,
f / (
(bound_in H),
m9)
|= the_scope_of H
by A28, A139, A144;
hence
contradiction
by A7, A147, ZF_LANG1:71;
verum
end; end;
now ( not bound_in H in Free (the_scope_of H) implies S1[H] )assume A157:
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 A26, A27;
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 A158:
(
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
A159:
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, A159, ZF_MODEL:16;
then
L . a,
f |= the_scope_of H
by A28, A158;
hence
L . a,
f |= H
by A7, A157, ZFMODEL1:10;
verum
end;
A160:
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, A160, ZF_MODEL:16;
then
Union L,
(Union L) ! f |= the_scope_of H
by A28, A158;
hence
Union L,
(Union L) ! f |= H
by A7, A157, ZFMODEL1:10;
verum
end; end;
hence
S1[
H]
by A137;
verum
end;
A161:
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 A162:
H = (the_left_argument_of H) '&' (the_right_argument_of H)
by ZF_LANG:40;
given fi1 being
Ordinal-Sequence of
W such that A163:
fi1 is
increasing
and A164:
fi1 is
continuous
and A165:
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 A166:
fi2 is
increasing
and A167:
fi2 is
continuous
and A168:
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 A163, A166, ORDINAL4:13;
hence
(
phi is
increasing &
phi is
continuous )
by A163, A164, A167, 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 A169:
phi . a = a
and A170:
{} <> 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:34;
then A171:
a c= fi1 . a
by A163, ORDINAL4:10;
let f be
Function of
VAR,
(L . a);
( Union L,(Union L) ! f |= H iff L . a,f |= H )
A172:
a in dom phi
by ORDINAL4:34;
A173:
a in dom fi2
by ORDINAL4:34;
A174:
now not fi1 . a <> aend;
then A177:
fi2 . a = a
by A169, A172, FUNCT_1:12;
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 A178:
Union L,
(Union L) ! f |= H
;
L . a,f |= H
then
Union L,
(Union L) ! f |= the_right_argument_of H
by A162, ZF_MODEL:15;
then A179:
L . a,
f |= the_right_argument_of H
by A168, A170, A177;
Union L,
(Union L) ! f |= the_left_argument_of H
by A162, A178, ZF_MODEL:15;
then
L . a,
f |= the_left_argument_of H
by A165, A170, A174;
hence
L . a,
f |= H
by A162, A179, ZF_MODEL:15;
verum
end;
assume A180:
L . a,
f |= H
;
Union L,(Union L) ! f |= H
then
L . a,
f |= the_right_argument_of H
by A162, ZF_MODEL:15;
then A181:
Union L,
(Union L) ! f |= the_right_argument_of H
by A168, A170, A177;
L . a,
f |= the_left_argument_of H
by A162, A180, ZF_MODEL:15;
then
Union L,
(Union L) ! f |= the_left_argument_of H
by A165, A170, A174;
hence
Union L,
(Union L) ! f |= H
by A162, A181, ZF_MODEL:15;
verum
end;
A182:
for H being ZF-formula st H is atomic holds
S1[H]
proof
A183:
dom (id (On W)) = On W
;
then reconsider phi =
id (On W) as
Sequence by ORDINAL1:def 7;
A184:
rng (id (On W)) = On W
;
reconsider phi =
phi as
Ordinal-Sequence ;
reconsider phi =
phi as
Ordinal-Sequence of
W by A183, A184, FUNCT_2:def 1, RELSET_1:4;
let H be
ZF-formula;
( H is atomic implies S1[H] )
assume A185:
(
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 A186:
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 13 for b1 being set holds
( not A in dom phi or A = 0 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 dom phi or A = 0 or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )
assume that A188:
A in dom phi
and A189:
(
A <> 0 &
A is
limit_ordinal )
and A190:
B = phi . A
;
B is_limes_of phi | A
A191:
A c= dom phi
by A188, ORDINAL1:def 2;
phi | A =
phi * (id A)
by RELAT_1:65
.=
id ((dom phi) /\ A)
by FUNCT_1:22
.=
id A
by A191, XBOOLE_1:28
;
then A192:
rng (phi | A) = A
;
phi . A = A
by A188, FUNCT_1:18;
then A193:
sup (phi | A) = B
by A190, A192, ORDINAL2:18;
A194:
phi | A is
increasing
by A186, ORDINAL4:15;
dom (phi | A) = A
by A191, RELAT_1:62;
hence
B is_limes_of phi | A
by A189, A193, A194, 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 A200:
L . a,
f |= H
;
Union L,(Union L) ! f |= H
A201:
(Union L) ! f = f
by Th16, ZF_LANG1:def 1;
hence
Union L,
(Union L) ! f |= H
by A185, A202;
verum
end;
A205:
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 A206:
H = 'not' (the_argument_of H)
by ZF_LANG:def 30;
given phi being
Ordinal-Sequence of
W such that A207:
(
phi is
increasing &
phi is
continuous )
and A208:
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 A207;
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 A209:
(
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 A206, ZF_MODEL:14;
then
not
Union L,
(Union L) ! f |= the_argument_of H
by A208, A209;
hence
Union L,
(Union L) ! f |= H
by A206, ZF_MODEL:14;
verum
end;
thus
for H being ZF-formula holds S1[H]
from ZF_LANG:sch 1(A182, A205, A161, A6); verum