let H be ZF-formula; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 )))))
; :: thesis: ( {(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;
then A5:
Free H = Free (H / (x. 0 ),x)
by A1, ZFMODEL2:2;
thus
{(x. 0 ),(x. 1),(x. 2)} misses Free (H / (x. 0 ),x)
by A1, A2, A4, ZFMODEL2:2; :: thesis: ( 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 )
A6:
not x. 0 in Free (H / (x. 0 ),x)
by A1, A4, ZFMODEL2:2;
now let m3 be
Element of
M;
:: thesis: 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:20;
take m0 =
m0;
:: thesis: 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;
:: thesis: ( ( 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 )
:: thesis: ( 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
;
:: thesis: 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:13;
then
M,
(v / (x. 3),m3) / (x. 4),
m4 |= H
by A4, ZFMODEL2:10;
hence
m4 = m0
by A7;
:: thesis: verum
end; assume
m4 = m0
;
:: thesis: M,(v / (x. 3),m3) / (x. 4),m4 |= H / (x. 0 ),xthen
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:10;
hence
M,
(v / (x. 3),m3) / (x. 4),
m4 |= H / (x. 0 ),
x
by A1, ZFMODEL2:13;
:: thesis: verum end;
hence A8:
M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),((H / (x. 0 ),x) <=> ((x. 4) '=' (x. 0 )))))
by A4, A5, ZFMODEL2:20; :: thesis: def_func' H,v = def_func' (H / (x. 0 ),x),v
now let u be
set ;
:: thesis: ( u in M implies (def_func' H,v) . u = (def_func' (H / (x. 0 ),x),v) . u )assume
u in M
;
:: thesis: (def_func' H,v) . u = (def_func' (H / (x. 0 ),x),v) . uthen reconsider u' =
u as
Element of
M ;
set m =
(def_func' H,v) . u';
M,
(v / (x. 3),u') / (x. 4),
((def_func' H,v) . u') |= H
by A3, A4, ZFMODEL2:11;
then
M,
((v / (x. 3),u') / (x. 4),((def_func' H,v) . u')) / (x. 0 ),
(((v / (x. 3),u') / (x. 4),((def_func' H,v) . u')) . x) |= H
by A4, ZFMODEL2:10;
then
M,
(v / (x. 3),u') / (x. 4),
((def_func' H,v) . u') |= H / (x. 0 ),
x
by A1, ZFMODEL2:13;
hence
(def_func' H,v) . u = (def_func' (H / (x. 0 ),x),v) . u
by A6, A8, ZFMODEL2:11;
:: thesis: verum end;
hence
def_func' H,v = def_func' (H / (x. 0 ),x),v
by FUNCT_2:18; :: thesis: verum