let x, y be Variable; :: thesis: 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 & y <> x. 3 & y <> x. 4 & 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 ; :: thesis: 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 & y <> x. 3 & y <> x. 4 & 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; :: thesis: 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 & y <> x. 3 & y <> x. 4 & 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; :: thesis: ( 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 & y <> x. 3 & y <> x. 4 & 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)) ) )
set F = H / y,x;
set f = v / x,(v . y);
assume that
A1:
( not x. 0 in Free H & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) )
and
A2:
( not x in variables_in H & y <> x. 3 & y <> x. 4 & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 )
; :: thesis: ( 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 A1, A2, 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 A3:
not x. 0 in Free (H / y,x)
; :: thesis: ( 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)) )
A4:
( x. 0 <> x. 3 & x. 0 <> x. 4 & x. 3 <> x. 4 )
by ZF_LANG1:86;
now let m3 be
Element of
M;
:: thesis: 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 A1, ZF_LANG1:80;
then consider m being
Element of
M such that A5:
M,
(v / (x. 3),m3) / (x. 0 ),
m |= All (x. 4),
(H <=> ((x. 4) '=' (x. 0 )))
by ZF_LANG1:82;
set f1 =
((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),
m;
now let m4 be
Element of
M;
:: thesis: M,(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= (H / y,x) <=> ((x. 4) '=' (x. 0 ))A6:
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H <=> ((x. 4) '=' (x. 0 ))
by A5, ZF_LANG1:80;
A7:
(
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = m4 &
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 0 ) = ((v / (x. 3),m3) / (x. 0 ),m) . (x. 0 ) &
((v / (x. 3),m3) / (x. 0 ),m) . (x. 0 ) = m &
((((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = m4 &
((((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 ) &
(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) . (x. 0 ) = m )
by A4, FUNCT_7:34, FUNCT_7:130;
A8:
now assume
M,
(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H / y,
x
;
:: thesis: 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 A2, Th13;
then
M,
(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H
by A2, Th10;
then
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
(v . y) |= H
by A2, A4, Th8;
then
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H
by A2, Th6;
then
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= (x. 4) '=' (x. 0 )
by A6, ZF_MODEL:19;
then
m = m4
by A7, ZF_MODEL:12;
hence
M,
(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= (x. 4) '=' (x. 0 )
by A7, ZF_MODEL:12;
:: thesis: verum end; now assume
M,
(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= (x. 4) '=' (x. 0 )
;
:: thesis: M,(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= H / y,xthen
m = m4
by A7, ZF_MODEL:12;
then
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= (x. 4) '=' (x. 0 )
by A7, ZF_MODEL:12;
then
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H
by A6, ZF_MODEL:19;
then
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
(v . y) |= H
by A2, Th6;
then
M,
(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H
by A2, A4, Th8;
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 A2, Th10;
hence
M,
(((v / x,(v . y)) / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H / y,
x
by A2, Th13;
:: thesis: 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 A8, ZF_MODEL:19;
:: thesis: 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:80;
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:82;
:: thesis: verum end;
hence A9:
M,v / x,(v . y) |= All (x. 3),(Ex (x. 0 ),(All (x. 4),((H / y,x) <=> ((x. 4) '=' (x. 0 )))))
by ZF_LANG1:80; :: thesis: def_func' H,v = def_func' (H / y,x),(v / x,(v . y))
let a be Element of M; :: according to FUNCT_2:def 9 :: thesis: (def_func' H,v) . a = (def_func' (H / y,x),(v / x,(v . y))) . a
set a' = (def_func' H,v) . a;
M,(v / (x. 3),a) / (x. 4),((def_func' H,v) . a) |= H
by A1, Th11;
then
M,((v / (x. 3),a) / (x. 4),((def_func' H,v) . a)) / x,(v . y) |= H
by A2, Th6;
then
M,((v / x,(v . y)) / (x. 3),a) / (x. 4),((def_func' H,v) . a) |= H
by A2, A4, Th7;
then A10:
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 A2, Th14;
( Free (H / y,x) = Free H & Free H c= variables_in H )
by A2, Th2, ZF_LANG1:164;
then
not x in Free (H / y,x)
by A2;
then
M,((v / x,(v . y)) / (x. 3),a) / (x. 4),((def_func' H,v) . a) |= H / y,x
by A10, Th10;
hence
(def_func' H,v) . a = (def_func' (H / y,x),(v / x,(v . y))) . a
by A3, A9, Th11; :: thesis: verum