let H be ZF-formula; for M being non empty set
for v being Function of VAR,M
for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
let M be non empty set ; for v being Function of VAR,M
for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
let v be Function of VAR,M; for x being Variable st not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
let x be Variable; ( not x in variables_in H & {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) ) )
assume that
A1:
not x in variables_in H
and
A2:
{(x. 0),(x. 1),(x. 2)} misses Free H
and
A3:
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
; ( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
x. 0 in {(x. 0),(x. 1),(x. 2)}
by ENUMSET1:def 1;
then A4:
not x. 0 in Free H
by A2, XBOOLE_0:3;
hence
{(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x))
by A1, A2, ZFMODEL2:2; ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
A5:
not x. 0 in Free (H / ((x. 0),x))
by A1, A4, ZFMODEL2:2;
A6:
now for m3 being Element of M ex m0 being Element of M st
for m4 being Element of M holds
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) )let m3 be
Element of
M;
ex m0 being Element of M st
for m4 being Element of M holds
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) )consider m0 being
Element of
M such that A7:
for
m being
Element of
M holds
(
M,
(v / ((x. 3),m3)) / (
(x. 4),
m)
|= H iff
m = m0 )
by A3, A4, ZFMODEL2:19;
take m0 =
m0;
for m4 being Element of M holds
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) )let m4 be
Element of
M;
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) implies m4 = m0 ) & ( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) ) )thus
(
M,
(v / ((x. 3),m3)) / (
(x. 4),
m4)
|= H / (
(x. 0),
x) implies
m4 = m0 )
( m4 = m0 implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x) )proof
assume
M,
(v / ((x. 3),m3)) / (
(x. 4),
m4)
|= H / (
(x. 0),
x)
;
m4 = m0
then
M,
((v / ((x. 3),m3)) / ((x. 4),m4)) / (
(x. 0),
(((v / ((x. 3),m3)) / ((x. 4),m4)) . x))
|= H
by A1, ZFMODEL2:12;
then
M,
(v / ((x. 3),m3)) / (
(x. 4),
m4)
|= H
by A4, ZFMODEL2:9;
hence
m4 = m0
by A7;
verum
end; assume
m4 = m0
;
M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H / ((x. 0),x)then
M,
(v / ((x. 3),m3)) / (
(x. 4),
m4)
|= H
by A7;
then
M,
((v / ((x. 3),m3)) / ((x. 4),m4)) / (
(x. 0),
(((v / ((x. 3),m3)) / ((x. 4),m4)) . x))
|= H
by A4, ZFMODEL2:9;
hence
M,
(v / ((x. 3),m3)) / (
(x. 4),
m4)
|= H / (
(x. 0),
x)
by A1, ZFMODEL2:12;
verum end;
Free H = Free (H / ((x. 0),x))
by A1, A4, ZFMODEL2:2;
hence A8:
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0))))))))
by A4, A6, ZFMODEL2:19; def_func' (H,v) = def_func' ((H / ((x. 0),x)),v)
now for u being object st u in M holds
(def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . ulet u be
object ;
( u in M implies (def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . u )assume
u in M
;
(def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . uthen reconsider u9 =
u as
Element of
M ;
set m =
(def_func' (H,v)) . u9;
M,
(v / ((x. 3),u9)) / (
(x. 4),
((def_func' (H,v)) . u9))
|= H
by A3, A4, ZFMODEL2:10;
then
M,
((v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9))) / (
(x. 0),
(((v / ((x. 3),u9)) / ((x. 4),((def_func' (H,v)) . u9))) . x))
|= H
by A4, ZFMODEL2:9;
then
M,
(v / ((x. 3),u9)) / (
(x. 4),
((def_func' (H,v)) . u9))
|= H / (
(x. 0),
x)
by A1, ZFMODEL2:12;
hence
(def_func' (H,v)) . u = (def_func' ((H / ((x. 0),x)),v)) . u
by A5, A8, ZFMODEL2:10;
verum end;
hence
def_func' (H,v) = def_func' ((H / ((x. 0),x)),v)
by FUNCT_2:12; verum