let x, y be Variable; for M being non empty set
for H being ZF-formula
for v being Function of VAR,M st not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x in variables_in H & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 holds
( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
let M be non empty set ; for H being ZF-formula
for v being Function of VAR,M st not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x in variables_in H & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 holds
( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
let H be ZF-formula; for v being Function of VAR,M st not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x in variables_in H & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 holds
( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
let v be Function of VAR,M; ( not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x in variables_in H & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 implies ( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) ) )
A1:
x. 0 <> x. 4
by ZF_LANG1:76;
A2:
x. 3 <> x. 4
by ZF_LANG1:76;
set F = H / (y,x);
set f = v / (x,(v . y));
assume that
A3:
not x. 0 in Free H
and
A4:
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
and
A5:
not x in variables_in H
and
A6:
not y in Free H
and
A7:
x <> x. 0
and
A8:
x <> x. 3
and
A9:
x <> x. 4
; ( not x. 0 in Free (H / (y,x)) & M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
( ( Free (H / (y,x)) c= variables_in (H / (y,x)) & not x. 0 in variables_in (H / (y,x)) ) or ( not x. 0 in {x} & not x. 0 in (Free H) \ {y} ) )
by A3, A7, TARSKI:def 1, XBOOLE_0:def 5;
then
( not x. 0 in Free (H / (y,x)) or ( Free (H / (y,x)) c= ((Free H) \ {y}) \/ {x} & not x. 0 in ((Free H) \ {y}) \/ {x} ) )
by Th1, XBOOLE_0:def 3;
hence A10:
not x. 0 in Free (H / (y,x))
; ( M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y)))) )
A11:
x. 0 <> x. 3
by ZF_LANG1:76;
now for m3 being Element of M holds M,(v / (x,(v . y))) / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0))))))let m3 be
Element of
M;
M,(v / (x,(v . y))) / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0))))))
M,
v / (
(x. 3),
m3)
|= Ex (
(x. 0),
(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))
by A4, ZF_LANG1:71;
then consider m being
Element of
M such that A12:
M,
(v / ((x. 3),m3)) / (
(x. 0),
m)
|= All (
(x. 4),
(H <=> ((x. 4) '=' (x. 0))))
by ZF_LANG1:73;
set f1 =
((v / (x,(v . y))) / ((x. 3),m3)) / (
(x. 0),
m);
now for m4 being Element of M holds M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (H / (y,x)) <=> ((x. 4) '=' (x. 0))let m4 be
Element of
M;
M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (H / (y,x)) <=> ((x. 4) '=' (x. 0))A13:
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4
by FUNCT_7:128;
A14:
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0)
by FUNCT_7:32, ZF_LANG1:76;
A15:
((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = (((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) . (x. 0)
by FUNCT_7:32, ZF_LANG1:76;
A16:
((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4
by FUNCT_7:128;
A17:
(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m
by FUNCT_7:128;
A18:
((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m
by FUNCT_7:128;
A19:
M,
((v / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H <=> ((x. 4) '=' (x. 0))
by A12, ZF_LANG1:71;
A20:
now ( M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) implies M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x) )assume
M,
(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= (x. 4) '=' (x. 0)
;
M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x)then
m = m4
by A16, A15, A17, ZF_MODEL:12;
then
M,
((v / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= (x. 4) '=' (x. 0)
by A13, A14, A18, ZF_MODEL:12;
then
M,
((v / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H
by A19, ZF_MODEL:19;
then
M,
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (
x,
(v . y))
|= H
by A5, Th5;
then
M,
(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H
by A7, A8, A9, A11, A1, A2, Th7;
then
M,
((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (
y,
(((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . x))
|= H
by A6, Th9;
hence
M,
(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H / (
y,
x)
by A5, Th12;
verum end; now ( M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x) implies M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) )assume
M,
(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H / (
y,
x)
;
M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0)then
M,
((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (
y,
(((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . x))
|= H
by A5, Th12;
then
M,
(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H
by A6, Th9;
then
M,
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (
x,
(v . y))
|= H
by A7, A8, A9, A11, A1, A2, Th7;
then
M,
((v / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H
by A5, Th5;
then
M,
((v / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= (x. 4) '=' (x. 0)
by A19, ZF_MODEL:19;
then
m = m4
by A13, A14, A18, ZF_MODEL:12;
hence
M,
(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= (x. 4) '=' (x. 0)
by A16, A15, A17, ZF_MODEL:12;
verum end; hence
M,
(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m4)
|= (H / (y,x)) <=> ((x. 4) '=' (x. 0))
by A20, ZF_MODEL:19;
verum end; then
M,
((v / (x,(v . y))) / ((x. 3),m3)) / (
(x. 0),
m)
|= All (
(x. 4),
((H / (y,x)) <=> ((x. 4) '=' (x. 0))))
by ZF_LANG1:71;
hence
M,
(v / (x,(v . y))) / (
(x. 3),
m3)
|= Ex (
(x. 0),
(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0))))))
by ZF_LANG1:73;
verum end;
hence A21:
M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0))))))))
by ZF_LANG1:71; def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y))))
A22:
Free H c= variables_in H
by ZF_LANG1:151;
Free (H / (y,x)) = Free H
by A5, A6, Th2;
then A23:
not x in Free (H / (y,x))
by A5, A22;
let a be Element of M; FUNCT_2:def 8 (def_func' (H,v)) . a = (def_func' ((H / (y,x)),(v / (x,(v . y))))) . a
set a9 = (def_func' (H,v)) . a;
M,(v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H
by A3, A4, Th10;
then
M,((v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) / (x,(v . y)) |= H
by A5, Th5;
then
M,((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H
by A8, A9, A2, Th6;
then
M,(((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) / (x,((((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) . y)) |= H / (y,x)
by A5, Th13;
then
M,((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H / (y,x)
by A23, Th9;
hence
(def_func' (H,v)) . a = (def_func' ((H / (y,x)),(v / (x,(v . y))))) . a
by A10, A21, Th10; verum