let M be non empty set ; for i being Element of NAT
for H1 being ZF-formula
for v1 being Function of VAR,M st not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H1,v1) = def_func' (H2,v2) )
let i be Element of NAT ; for H1 being ZF-formula
for v1 being Function of VAR,M st not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H1,v1) = def_func' (H2,v2) )
let H1 be ZF-formula; for v1 being Function of VAR,M st not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H1,v1) = def_func' (H2,v2) )
let v1 be Function of VAR,M; ( not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H1,v1) = def_func' (H2,v2) ) )
defpred S1[ ZF-formula, Nat] means for v1 being Function of VAR,M st not x. 0 in Free $1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),($1 <=> ((x. 4) '=' (x. 0)))))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < $2 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' ($1,v1) = def_func' (H2,v2) );
defpred S2[ Nat] means for H being ZF-formula holds S1[H,$1];
A1:
for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be
Nat;
( S2[i] implies S2[i + 1] )
assume A2:
for
H being
ZF-formula holds
S1[
H,
i]
;
S2[i + 1]
let H be
ZF-formula;
S1[H,i + 1]let v1 be
Function of
VAR,
M;
( not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) )
assume that A3:
not
x. 0 in Free H
and A4:
M,
v1 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
;
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
A5:
(
i = 0 implies ex
H2 being
ZF-formula ex
v2 being
Function of
VAR,
M st
( ( for
j being
Element of
NAT st
j < i + 1 &
x. j in variables_in H2 & not
j = 3 holds
j = 4 ) & not
x. 0 in Free H2 &
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H,
v1)
= def_func' (
H2,
v2) ) )
proof
assume A6:
i = 0
;
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
consider k being
Element of
NAT such that A7:
for
j being
Element of
NAT st
x. j in variables_in H holds
j < k
by Th3;
(
k > 4 or not
k > 4 )
;
then consider k1 being
Element of
NAT such that A8:
( (
k > 4 &
k1 = k ) or ( not
k > 4 &
k1 = 5 ) )
;
take F =
H / (
(x. 0),
(x. k1));
ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 ) & not x. 0 in Free F & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,v2) )
take
v1 / (
(x. k1),
(v1 . (x. 0)))
;
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 ) & not x. 0 in Free F & M,v1 / ((x. k1),(v1 . (x. 0))) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,(v1 / ((x. k1),(v1 . (x. 0))))) )
thus
for
j being
Element of
NAT st
j < i + 1 &
x. j in variables_in F & not
j = 3 holds
j = 4
( not x. 0 in Free F & M,v1 / ((x. k1),(v1 . (x. 0))) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,(v1 / ((x. k1),(v1 . (x. 0))))) )
A9:
x. k1 <> x. 0
by A8, ZF_LANG1:76;
k1 <> 3
by A8;
then A10:
x. k1 <> x. 3
by ZF_LANG1:76;
A11:
x. k1 <> x. 4
by A8, ZF_LANG1:76;
not
x. k1 in variables_in H
by A7, A8, XXREAL_0:2;
hence
( not
x. 0 in Free F &
M,
v1 / (
(x. k1),
(v1 . (x. 0)))
|= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H,
v1)
= def_func' (
F,
(v1 / ((x. k1),(v1 . (x. 0))))) )
by A3, A4, A9, A10, A11, Th14;
verum
end;
A12:
(
i <> 0 &
i <> 3 &
i <> 4 implies ex
H2 being
ZF-formula ex
v2 being
Function of
VAR,
M st
( ( for
j being
Element of
NAT st
j < i + 1 &
x. j in variables_in H2 & not
j = 3 holds
j = 4 ) & not
x. 0 in Free H2 &
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H,
v1)
= def_func' (
H2,
v2) ) )
proof
A13:
x. 3
<> x. 4
by ZF_LANG1:76;
assume that A14:
i <> 0
and A15:
i <> 3
and A16:
i <> 4
;
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
reconsider ii =
i as
Element of
NAT by ORDINAL1:def 12;
A17:
x. 0 <> x. ii
by A14, ZF_LANG1:76;
consider H1 being
ZF-formula,
v9 being
Function of
VAR,
M such that A18:
for
j being
Element of
NAT st
j < i &
x. j in variables_in H1 & not
j = 3 holds
j = 4
and A19:
not
x. 0 in Free H1
and A20:
M,
v9 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))
and A21:
def_func' (
H,
v1)
= def_func' (
H1,
v9)
by A2, A3, A4;
consider k being
Element of
NAT such that A22:
for
j being
Element of
NAT st
x. j in variables_in (All ((x. 4),(x. ii),H1)) holds
j < k
by Th3;
take H2 =
H1 / (
(x. ii),
(x. k));
ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
take v2 =
v9 / (
(x. k),
(v9 . (x. ii)));
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
A23:
variables_in (All ((x. 4),(x. ii),H1)) = (variables_in H1) \/ {(x. 4),(x. ii)}
by ZF_LANG1:147;
x. ii in {(x. 4),(x. ii)}
by TARSKI:def 2;
then A24:
x. ii in variables_in (All ((x. 4),(x. ii),H1))
by A23, XBOOLE_0:def 3;
then A25:
x. ii <> x. k
by A22;
then A26:
v2 / (
(x. ii),
(v2 . (x. k)))
= (v9 / ((x. ii),(v2 . (x. k)))) / (
(x. k),
(v9 . (x. ii)))
by FUNCT_7:33;
thus
for
j being
Element of
NAT st
j < i + 1 &
x. j in variables_in H2 & not
j = 3 holds
j = 4
( not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )proof
x. ii in {(x. ii)}
by TARSKI:def 1;
then A27:
not
x. ii in (variables_in H1) \ {(x. ii)}
by XBOOLE_0:def 5;
A28:
not
x. ii in {(x. k)}
by A25, TARSKI:def 1;
let j be
Element of
NAT ;
( j < i + 1 & x. j in variables_in H2 & not j = 3 implies j = 4 )
A29:
variables_in H2 c= ((variables_in H1) \ {(x. ii)}) \/ {(x. k)}
by ZF_LANG1:187;
assume
j < i + 1
;
( not x. j in variables_in H2 or j = 3 or j = 4 )
then A30:
j <= i
by NAT_1:13;
then
j < k
by A22, A24, XXREAL_0:2;
then A31:
x. j <> x. k
by ZF_LANG1:76;
assume A32:
x. j in variables_in H2
;
( j = 3 or j = 4 )
then
(
x. j in (variables_in H1) \ {(x. ii)} or
x. j in {(x. k)} )
by A29, XBOOLE_0:def 3;
then A33:
x. j in variables_in H1
by A31, TARSKI:def 1, XBOOLE_0:def 5;
(
j = i or
j < i )
by A30, XXREAL_0:1;
hence
(
j = 3 or
j = 4 )
by A18, A27, A28, A29, A32, A33, XBOOLE_0:def 3;
verum
end;
A34:
v2 . (x. k) = v9 . (x. ii)
by FUNCT_7:128;
A35:
Free H2 c= ((Free H1) \ {(x. ii)}) \/ {(x. k)}
by Th1;
A36:
x. 4
<> x. ii
by A16, ZF_LANG1:76;
A37:
x. 3
<> x. ii
by A15, ZF_LANG1:76;
then A38:
(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) / (
(x. ii),
(x. k)) =
All (
(x. 3),
((Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))) / ((x. ii),(x. k))))
by ZF_LANG1:159
.=
All (
(x. 3),
(Ex ((x. 0),((All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))) / ((x. ii),(x. k))))))
by A17, ZF_LANG1:164
.=
All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),((H1 <=> ((x. 4) '=' (x. 0))) / ((x. ii),(x. k))))))))
by A36, ZF_LANG1:159
.=
All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> (((x. 4) '=' (x. 0)) / ((x. ii),(x. k)))))))))
by ZF_LANG1:163
.=
All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0))))))))
by A17, A36, ZF_LANG1:152
;
A39:
v9 / (
(x. ii),
(v9 . (x. ii)))
= v9
by FUNCT_7:35;
A40:
not
x. 0 in (Free H1) \ {(x. ii)}
by A19, XBOOLE_0:def 5;
not
x. k in variables_in (All ((x. 4),(x. ii),H1))
by A22;
then A41:
not
x. k in variables_in H1
by A23, XBOOLE_0:def 3;
x. 4
in {(x. 4),(x. ii)}
by TARSKI:def 2;
then A42:
x. 4
in variables_in (All ((x. 4),(x. ii),H1))
by A23, XBOOLE_0:def 3;
then A43:
x. 4
<> x. k
by A22;
then A44:
not
x. k in {(x. 4)}
by TARSKI:def 1;
A45:
0 <> k
by A22, A42;
then A46:
x. 0 <> x. k
by ZF_LANG1:76;
then A47:
not
x. k in {(x. 0)}
by TARSKI:def 1;
not
x. k in {(x. 4),(x. 0)}
by A46, A43, TARSKI:def 2;
then
not
x. k in (variables_in H1) \/ {(x. 4),(x. 0)}
by A41, XBOOLE_0:def 3;
then
not
x. k in ((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}
by A44, XBOOLE_0:def 3;
then A48:
not
x. k in (((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)}
by A47, XBOOLE_0:def 3;
A49:
x. 0 <> x. 3
by ZF_LANG1:76;
A50:
not
x. 0 in {(x. k)}
by A46, TARSKI:def 1;
then A51:
not
x. 0 in Free H2
by A40, A35, XBOOLE_0:def 3;
thus
not
x. 0 in Free H2
by A40, A50, A35, XBOOLE_0:def 3;
( M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
A52:
variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) =
(variables_in (Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) \/ {(x. 3)}
by ZF_LANG1:142
.=
((variables_in (All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))) \/ {(x. 0)}) \/ {(x. 3)}
by ZF_LANG1:146
.=
(((variables_in (H1 <=> ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)}
by ZF_LANG1:142
.=
((((variables_in H1) \/ (variables_in ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)}
by ZF_LANG1:145
.=
((((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)}
by ZF_LANG1:138
;
A53:
x. 0 <> x. 4
by ZF_LANG1:76;
A54:
3
<> k
by A22, A42;
then A55:
x. 3
<> x. k
by ZF_LANG1:76;
then
not
x. k in {(x. 3)}
by TARSKI:def 1;
then A56:
not
x. k in variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))))
by A52, A48, XBOOLE_0:def 3;
then
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))
by A20, Th5;
hence A57:
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0))))))))
by A38, A56, A34, A39, A26, Th12;
def_func' (H,v1) = def_func' (H2,v2)
now for e being Element of M holds (def_func' (H2,v2)) . e = (def_func' (H1,v9)) . elet e be
Element of
M;
(def_func' (H2,v2)) . e = (def_func' (H1,v9)) . eA58:
v2 . (x. k) = v9 . (x. ii)
by FUNCT_7:128;
A59:
(v2 / ((x. 3),e)) . (x. k) = v2 . (x. k)
by A54, FUNCT_7:32, ZF_LANG1:76;
M,
v9 / (
(x. 3),
e)
|= Ex (
(x. 0),
(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))
by A20, ZF_LANG1:71;
then consider e9 being
Element of
M such that A60:
M,
(v9 / ((x. 3),e)) / (
(x. 0),
e9)
|= All (
(x. 4),
(H1 <=> ((x. 4) '=' (x. 0))))
by ZF_LANG1:73;
A61:
(((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9)) . (x. 0) = ((v9 / ((x. 3),e)) / ((x. 0),e9)) . (x. 0)
by FUNCT_7:32, ZF_LANG1:76;
A62:
((v9 / ((x. 3),e)) / ((x. 0),e9)) . (x. 0) = e9
by FUNCT_7:128;
(((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9)) . (x. 4) = e9
by FUNCT_7:128;
then A63:
M,
((v9 / ((x. 3),e)) / ((x. 0),e9)) / (
(x. 4),
e9)
|= (x. 4) '=' (x. 0)
by A61, A62, ZF_MODEL:12;
A64:
M,
((v9 / ((x. 3),e)) / ((x. 0),e9)) / (
(x. 4),
e9)
|= H1 <=> ((x. 4) '=' (x. 0))
by A60, ZF_LANG1:71;
then A65:
M,
((v9 / ((x. 3),e)) / ((x. 0),e9)) / (
(x. 4),
e9)
|= H1
by A63, ZF_MODEL:19;
A66:
(v2 / ((x. 3),e)) . (x. k) = ((v2 / ((x. 3),e)) / ((x. 4),e9)) . (x. k)
by A43, FUNCT_7:32;
A67:
(((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) . (x. k) = ((v2 / ((x. 3),e)) / ((x. 4),e9)) . (x. k)
by A45, FUNCT_7:32, ZF_LANG1:76;
A68:
((v9 / ((x. 3),e)) / ((x. 0),e9)) / (
(x. 4),
e9)
= ((v9 / ((x. 3),e)) / ((x. 4),e9)) / (
(x. 0),
e9)
by FUNCT_7:33, ZF_LANG1:76;
A69:
v2 / (
(x. ii),
(v2 . (x. k)))
= (v9 / ((x. ii),(v2 . (x. k)))) / (
(x. k),
(v9 . (x. ii)))
by A25, FUNCT_7:33;
A70:
v9 / (
(x. ii),
(v9 . (x. ii)))
= v9
by FUNCT_7:35;
((v2 / ((x. 3),e)) / ((x. 4),e9)) / (
(x. 0),
e9)
= (((v9 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) / (
(x. k),
(v9 . (x. ii)))
by A46, A55, A43, A49, A53, A13, Th7;
then A71:
M,
((v2 / ((x. 3),e)) / ((x. 4),e9)) / (
(x. 0),
e9)
|= H1
by A41, A65, A68, Th5;
(((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) / (
(x. ii),
(v2 . (x. k)))
= (((v2 / ((x. ii),(v2 . (x. k)))) / ((x. 3),e)) / ((x. 4),e9)) / (
(x. 0),
e9)
by A17, A37, A36, A49, A53, A13, Th7;
then
M,
((v2 / ((x. 3),e)) / ((x. 4),e9)) / (
(x. 0),
e9)
|= H2
by A41, A71, A67, A66, A59, A69, A58, A70, Th12;
then
M,
(v2 / ((x. 3),e)) / (
(x. 4),
e9)
|= H2
by A51, Th9;
then A72:
(def_func' (H2,v2)) . e = e9
by A51, A57, Th10;
M,
((v9 / ((x. 3),e)) / ((x. 4),e9)) / (
(x. 0),
e9)
|= H1
by A64, A63, A68, ZF_MODEL:19;
then
M,
(v9 / ((x. 3),e)) / (
(x. 4),
e9)
|= H1
by A19, Th9;
hence
(def_func' (H2,v2)) . e = (def_func' (H1,v9)) . e
by A19, A20, A72, Th10;
verum end;
hence
def_func' (
H2,
v2)
= def_func' (
H,
v1)
by A21;
verum
end;
now ( ( i = 3 or i = 4 ) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) )assume A73:
(
i = 3 or
i = 4 )
;
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )thus
ex
H2 being
ZF-formula ex
v2 being
Function of
VAR,
M st
( ( for
j being
Element of
NAT st
j < i + 1 &
x. j in variables_in H2 & not
j = 3 holds
j = 4 ) & not
x. 0 in Free H2 &
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H,
v1)
= def_func' (
H2,
v2) )
verumproof
consider H2 being
ZF-formula,
v2 being
Function of
VAR,
M such that A74:
for
j being
Element of
NAT st
j < i &
x. j in variables_in H2 & not
j = 3 holds
j = 4
and A75:
not
x. 0 in Free H2
and A76:
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0))))))))
and A77:
def_func' (
H,
v1)
= def_func' (
H2,
v2)
by A2, A3, A4;
take
H2
;
ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
take
v2
;
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
thus
for
j being
Element of
NAT st
j < i + 1 &
x. j in variables_in H2 & not
j = 3 holds
j = 4
( not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
thus
( not
x. 0 in Free H2 &
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H,
v1)
= def_func' (
H2,
v2) )
by A75, A76, A77;
verum
end; end;
hence
ex
H2 being
ZF-formula ex
v2 being
Function of
VAR,
M st
( ( for
j being
Element of
NAT st
j < i + 1 &
x. j in variables_in H2 & not
j = 3 holds
j = 4 ) & not
x. 0 in Free H2 &
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H,
v1)
= def_func' (
H2,
v2) )
by A12, A5;
verum
end;
A80:
S2[ 0 ]
proof
let H be
ZF-formula;
S1[H, 0 ]let v1 be
Function of
VAR,
M;
( not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < 0 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) )
assume that A81:
not
x. 0 in Free H
and A82:
M,
v1 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
;
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < 0 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
take
H
;
ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < 0 & x. j in variables_in H & not j = 3 holds
j = 4 ) & not x. 0 in Free H & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H,v2) )
take
v1
;
( ( for j being Element of NAT st j < 0 & x. j in variables_in H & not j = 3 holds
j = 4 ) & not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H,v1) )
thus
( ( for
j being
Element of
NAT st
j < 0 &
x. j in variables_in H & not
j = 3 holds
j = 4 ) & not
x. 0 in Free H &
M,
v1 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H,
v1)
= def_func' (
H,
v1) )
by A81, A82;
verum
end;
for i being Nat holds S2[i]
from NAT_1:sch 2(A80, A1);
hence
( not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H1,v1) = def_func' (H2,v2) ) )
; verum