let H be ZF-formula; for x, y being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds
( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
let x, y be Variable; ( not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 implies ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) ) )
A1:
x. 0 <> x. 3
by ZF_LANG1:76;
assume that
A2:
not y in variables_in H
and
A3:
x <> x. 0
and
A4:
y <> x. 0
and
A5:
y <> x. 4
; ( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
set G = (H / ((x. 0),y)) / ((x. 4),(x. 0));
A6: Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) =
(Free (((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)}
by ZF_LANG1:66
.=
((Free ((x. 3) 'in' x)) \/ (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)}
by ZF_LANG1:61
.=
({(x. 3),x} \/ (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))))) \ {(x. 3)}
by ZF_LANG1:59
.=
({(x. 3),x} \ {(x. 3)}) \/ ((Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)})
by XBOOLE_1:42
;
A7:
x. 0 <> x. 4
by ZF_LANG1:76;
A8:
now ( x. 4 in Free H implies x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )assume A9:
x. 4
in Free H
;
x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))))A10:
x. 4
in Free (H / ((x. 0),y))
A13:
x. 0 in {(x. 0)}
by TARSKI:def 1;
not
x. 0 in variables_in (H / ((x. 0),y))
by A4, ZF_LANG1:184;
then
Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) = ((Free (H / ((x. 0),y))) \ {(x. 4)}) \/ {(x. 0)}
by A10, ZFMODEL2:2;
then A14:
x. 0 in Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))
by A13, XBOOLE_0:def 3;
not
x. 0 in {(x. 3)}
by A1, TARSKI:def 1;
then
x. 0 in (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)}
by A14, XBOOLE_0:def 5;
hence
x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))))
by A6, XBOOLE_0:def 3;
verum end;
now ( x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) implies x. 4 in Free H )assume
x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0))))))
;
x. 4 in Free Hthen
(
x. 0 in {(x. 3),x} \ {(x. 3)} or
x. 0 in (Free ((H / ((x. 0),y)) / ((x. 4),(x. 0)))) \ {(x. 3)} )
by A6, XBOOLE_0:def 3;
then A15:
(
x. 0 in {(x. 3),x} or
x. 0 in Free ((H / ((x. 0),y)) / ((x. 4),(x. 0))) )
by XBOOLE_0:def 5;
A16:
not
x. 0 in variables_in (H / ((x. 0),y))
by A4, ZF_LANG1:184;
A17:
now x. 4 in Free (H / ((x. 0),y))assume
not
x. 4
in Free (H / ((x. 0),y))
;
contradictionthen A18:
x. 0 in Free (H / ((x. 0),y))
by A3, A1, A15, A16, TARSKI:def 2, ZFMODEL2:2;
Free (H / ((x. 0),y)) c= variables_in (H / ((x. 0),y))
by ZF_LANG1:151;
hence
contradiction
by A4, A18, ZF_LANG1:184;
verum end;
Free (H / ((x. 0),y)) c= ((Free H) \ {(x. 0)}) \/ {y}
by ZFMODEL2:1;
then
(
x. 4
in (Free H) \ {(x. 0)} or
x. 4
in {y} )
by A17, XBOOLE_0:def 3;
hence
x. 4
in Free H
by A5, TARSKI:def 1, XBOOLE_0:def 5;
verum end;
hence
( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
by A8; verum