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 in variables_in H holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )

let M be non empty set ; :: thesis: for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )

let H be ZF-formula; :: thesis: for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )

let v be Function of VAR,M; :: thesis: ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) )

defpred S_{1}[ ZF-formula] means ( not x in variables_in $1 implies for v being Function of VAR,M holds

( M,v |= $1 / (y,x) iff M,v / (y,(v . x)) |= $1 ) );

A1: for x1, x2 being Variable holds

( S_{1}[x1 '=' x2] & S_{1}[x1 'in' x2] )
_{1}[H1] & S_{1}[H2] holds

S_{1}[H1 '&' H2]

for z being Variable st S_{1}[H] holds

S_{1}[ All (z,H)]
_{1}[H] holds

S_{1}[ 'not' H]
_{1}[H]
from ZF_LANG1:sch 1(A1, A44, A12, A20);

hence ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: verum

for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )

let M be non empty set ; :: thesis: for H being ZF-formula

for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )

let H be ZF-formula; :: thesis: for v being Function of VAR,M st not x in variables_in H holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H )

let v be Function of VAR,M; :: thesis: ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) )

defpred S

( M,v |= $1 / (y,x) iff M,v / (y,(v . x)) |= $1 ) );

A1: for x1, x2 being Variable holds

( S

proof

A12:
for H1, H2 being ZF-formula st S
let x1, x2 be Variable; :: thesis: ( S_{1}[x1 '=' x2] & S_{1}[x1 'in' x2] )

A2: ( x2 = y or x2 <> y ) ;

A3: ( x1 = y or x1 <> y ) ;

thus S_{1}[x1 '=' x2]
:: thesis: S_{1}[x1 'in' x2]

A8: ( ( x1 <> y & x2 <> y & y1 = x1 & y2 = x2 ) or ( x1 = y & x2 <> y & y1 = x & y2 = x2 ) or ( x1 <> y & x2 = y & y1 = x1 & y2 = x ) or ( x1 = y & x2 = y & y1 = x & y2 = x ) ) by A3, A2;

assume not x in variables_in (x1 'in' x2) ; :: thesis: for v being Function of VAR,M holds

( M,v |= (x1 'in' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 'in' x2 )

let v be Function of VAR,M; :: thesis: ( M,v |= (x1 'in' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 'in' x2 )

A9: (v / (y,(v . x))) . x1 = v . y1 by A8, FUNCT_7:32, FUNCT_7:128;

A10: (v / (y,(v . x))) . x2 = v . y2 by A8, FUNCT_7:32, FUNCT_7:128;

A11: (x1 'in' x2) / (y,x) = y1 'in' y2 by A8, ZF_LANG1:154;

thus ( M,v |= (x1 'in' x2) / (y,x) implies M,v / (y,(v . x)) |= x1 'in' x2 ) :: thesis: ( M,v / (y,(v . x)) |= x1 'in' x2 implies M,v |= (x1 'in' x2) / (y,x) )

then (v / (y,(v . x))) . x1 in (v / (y,(v . x))) . x2 by ZF_MODEL:13;

hence M,v |= (x1 'in' x2) / (y,x) by A11, A9, A10, ZF_MODEL:13; :: thesis: verum

end;A2: ( x2 = y or x2 <> y ) ;

A3: ( x1 = y or x1 <> y ) ;

thus S

proof

consider y1, y2 being Variable such that
assume
not x in variables_in (x1 '=' x2)
; :: thesis: for v being Function of VAR,M holds

( M,v |= (x1 '=' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 '=' x2 )

let v be Function of VAR,M; :: thesis: ( M,v |= (x1 '=' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 '=' x2 )

consider y1, y2 being Variable such that

A4: ( ( x1 <> y & x2 <> y & y1 = x1 & y2 = x2 ) or ( x1 = y & x2 <> y & y1 = x & y2 = x2 ) or ( x1 <> y & x2 = y & y1 = x1 & y2 = x ) or ( x1 = y & x2 = y & y1 = x & y2 = x ) ) by A3, A2;

A5: (v / (y,(v . x))) . x2 = v . y2 by A4, FUNCT_7:32, FUNCT_7:128;

A6: (v / (y,(v . x))) . x1 = v . y1 by A4, FUNCT_7:32, FUNCT_7:128;

A7: (x1 '=' x2) / (y,x) = y1 '=' y2 by A4, ZF_LANG1:152;

thus ( M,v |= (x1 '=' x2) / (y,x) implies M,v / (y,(v . x)) |= x1 '=' x2 ) :: thesis: ( M,v / (y,(v . x)) |= x1 '=' x2 implies M,v |= (x1 '=' x2) / (y,x) )

then (v / (y,(v . x))) . x1 = (v / (y,(v . x))) . x2 by ZF_MODEL:12;

hence M,v |= (x1 '=' x2) / (y,x) by A7, A6, A5, ZF_MODEL:12; :: thesis: verum

end;( M,v |= (x1 '=' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 '=' x2 )

let v be Function of VAR,M; :: thesis: ( M,v |= (x1 '=' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 '=' x2 )

consider y1, y2 being Variable such that

A4: ( ( x1 <> y & x2 <> y & y1 = x1 & y2 = x2 ) or ( x1 = y & x2 <> y & y1 = x & y2 = x2 ) or ( x1 <> y & x2 = y & y1 = x1 & y2 = x ) or ( x1 = y & x2 = y & y1 = x & y2 = x ) ) by A3, A2;

A5: (v / (y,(v . x))) . x2 = v . y2 by A4, FUNCT_7:32, FUNCT_7:128;

A6: (v / (y,(v . x))) . x1 = v . y1 by A4, FUNCT_7:32, FUNCT_7:128;

A7: (x1 '=' x2) / (y,x) = y1 '=' y2 by A4, ZF_LANG1:152;

thus ( M,v |= (x1 '=' x2) / (y,x) implies M,v / (y,(v . x)) |= x1 '=' x2 ) :: thesis: ( M,v / (y,(v . x)) |= x1 '=' x2 implies M,v |= (x1 '=' x2) / (y,x) )

proof

assume
M,v / (y,(v . x)) |= x1 '=' x2
; :: thesis: M,v |= (x1 '=' x2) / (y,x)
assume
M,v |= (x1 '=' x2) / (y,x)
; :: thesis: M,v / (y,(v . x)) |= x1 '=' x2

then v . y1 = v . y2 by A7, ZF_MODEL:12;

hence M,v / (y,(v . x)) |= x1 '=' x2 by A6, A5, ZF_MODEL:12; :: thesis: verum

end;then v . y1 = v . y2 by A7, ZF_MODEL:12;

hence M,v / (y,(v . x)) |= x1 '=' x2 by A6, A5, ZF_MODEL:12; :: thesis: verum

then (v / (y,(v . x))) . x1 = (v / (y,(v . x))) . x2 by ZF_MODEL:12;

hence M,v |= (x1 '=' x2) / (y,x) by A7, A6, A5, ZF_MODEL:12; :: thesis: verum

A8: ( ( x1 <> y & x2 <> y & y1 = x1 & y2 = x2 ) or ( x1 = y & x2 <> y & y1 = x & y2 = x2 ) or ( x1 <> y & x2 = y & y1 = x1 & y2 = x ) or ( x1 = y & x2 = y & y1 = x & y2 = x ) ) by A3, A2;

assume not x in variables_in (x1 'in' x2) ; :: thesis: for v being Function of VAR,M holds

( M,v |= (x1 'in' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 'in' x2 )

let v be Function of VAR,M; :: thesis: ( M,v |= (x1 'in' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 'in' x2 )

A9: (v / (y,(v . x))) . x1 = v . y1 by A8, FUNCT_7:32, FUNCT_7:128;

A10: (v / (y,(v . x))) . x2 = v . y2 by A8, FUNCT_7:32, FUNCT_7:128;

A11: (x1 'in' x2) / (y,x) = y1 'in' y2 by A8, ZF_LANG1:154;

thus ( M,v |= (x1 'in' x2) / (y,x) implies M,v / (y,(v . x)) |= x1 'in' x2 ) :: thesis: ( M,v / (y,(v . x)) |= x1 'in' x2 implies M,v |= (x1 'in' x2) / (y,x) )

proof

assume
M,v / (y,(v . x)) |= x1 'in' x2
; :: thesis: M,v |= (x1 'in' x2) / (y,x)
assume
M,v |= (x1 'in' x2) / (y,x)
; :: thesis: M,v / (y,(v . x)) |= x1 'in' x2

then v . y1 in v . y2 by A11, ZF_MODEL:13;

hence M,v / (y,(v . x)) |= x1 'in' x2 by A9, A10, ZF_MODEL:13; :: thesis: verum

end;then v . y1 in v . y2 by A11, ZF_MODEL:13;

hence M,v / (y,(v . x)) |= x1 'in' x2 by A9, A10, ZF_MODEL:13; :: thesis: verum

then (v / (y,(v . x))) . x1 in (v / (y,(v . x))) . x2 by ZF_MODEL:13;

hence M,v |= (x1 'in' x2) / (y,x) by A11, A9, A10, ZF_MODEL:13; :: thesis: verum

S

proof

A20:
for H being ZF-formula
let H1, H2 be ZF-formula; :: thesis: ( S_{1}[H1] & S_{1}[H2] implies S_{1}[H1 '&' H2] )

assume that

A13: ( not x in variables_in H1 implies for v being Function of VAR,M holds

( M,v |= H1 / (y,x) iff M,v / (y,(v . x)) |= H1 ) ) and

A14: ( not x in variables_in H2 implies for v being Function of VAR,M holds

( M,v |= H2 / (y,x) iff M,v / (y,(v . x)) |= H2 ) ) ; :: thesis: S_{1}[H1 '&' H2]

assume not x in variables_in (H1 '&' H2) ; :: thesis: for v being Function of VAR,M holds

( M,v |= (H1 '&' H2) / (y,x) iff M,v / (y,(v . x)) |= H1 '&' H2 )

then A15: not x in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;

let v be Function of VAR,M; :: thesis: ( M,v |= (H1 '&' H2) / (y,x) iff M,v / (y,(v . x)) |= H1 '&' H2 )

thus ( M,v |= (H1 '&' H2) / (y,x) implies M,v / (y,(v . x)) |= H1 '&' H2 ) :: thesis: ( M,v / (y,(v . x)) |= H1 '&' H2 implies M,v |= (H1 '&' H2) / (y,x) )

then M,v / (y,(v . x)) |= H2 by ZF_MODEL:15;

then A19: M,v |= H2 / (y,x) by A14, A15, XBOOLE_0:def 3;

M,v / (y,(v . x)) |= H1 by A18, ZF_MODEL:15;

then M,v |= H1 / (y,x) by A13, A15, XBOOLE_0:def 3;

then M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by A19, ZF_MODEL:15;

hence M,v |= (H1 '&' H2) / (y,x) by ZF_LANG1:158; :: thesis: verum

end;assume that

A13: ( not x in variables_in H1 implies for v being Function of VAR,M holds

( M,v |= H1 / (y,x) iff M,v / (y,(v . x)) |= H1 ) ) and

A14: ( not x in variables_in H2 implies for v being Function of VAR,M holds

( M,v |= H2 / (y,x) iff M,v / (y,(v . x)) |= H2 ) ) ; :: thesis: S

assume not x in variables_in (H1 '&' H2) ; :: thesis: for v being Function of VAR,M holds

( M,v |= (H1 '&' H2) / (y,x) iff M,v / (y,(v . x)) |= H1 '&' H2 )

then A15: not x in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;

let v be Function of VAR,M; :: thesis: ( M,v |= (H1 '&' H2) / (y,x) iff M,v / (y,(v . x)) |= H1 '&' H2 )

thus ( M,v |= (H1 '&' H2) / (y,x) implies M,v / (y,(v . x)) |= H1 '&' H2 ) :: thesis: ( M,v / (y,(v . x)) |= H1 '&' H2 implies M,v |= (H1 '&' H2) / (y,x) )

proof

assume A18:
M,v / (y,(v . x)) |= H1 '&' H2
; :: thesis: M,v |= (H1 '&' H2) / (y,x)
assume
M,v |= (H1 '&' H2) / (y,x)
; :: thesis: M,v / (y,(v . x)) |= H1 '&' H2

then A16: M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by ZF_LANG1:158;

then M,v |= H2 / (y,x) by ZF_MODEL:15;

then A17: M,v / (y,(v . x)) |= H2 by A14, A15, XBOOLE_0:def 3;

M,v |= H1 / (y,x) by A16, ZF_MODEL:15;

then M,v / (y,(v . x)) |= H1 by A13, A15, XBOOLE_0:def 3;

hence M,v / (y,(v . x)) |= H1 '&' H2 by A17, ZF_MODEL:15; :: thesis: verum

end;then A16: M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by ZF_LANG1:158;

then M,v |= H2 / (y,x) by ZF_MODEL:15;

then A17: M,v / (y,(v . x)) |= H2 by A14, A15, XBOOLE_0:def 3;

M,v |= H1 / (y,x) by A16, ZF_MODEL:15;

then M,v / (y,(v . x)) |= H1 by A13, A15, XBOOLE_0:def 3;

hence M,v / (y,(v . x)) |= H1 '&' H2 by A17, ZF_MODEL:15; :: thesis: verum

then M,v / (y,(v . x)) |= H2 by ZF_MODEL:15;

then A19: M,v |= H2 / (y,x) by A14, A15, XBOOLE_0:def 3;

M,v / (y,(v . x)) |= H1 by A18, ZF_MODEL:15;

then M,v |= H1 / (y,x) by A13, A15, XBOOLE_0:def 3;

then M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by A19, ZF_MODEL:15;

hence M,v |= (H1 '&' H2) / (y,x) by ZF_LANG1:158; :: thesis: verum

for z being Variable st S

S

proof

A44:
for H being ZF-formula st S
let H be ZF-formula; :: thesis: for z being Variable st S_{1}[H] holds

S_{1}[ All (z,H)]

let z be Variable; :: thesis: ( S_{1}[H] implies S_{1}[ All (z,H)] )

assume A21: ( not x in variables_in H implies for v being Function of VAR,M holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: S_{1}[ All (z,H)]

( z = y or z <> y ) ;

then consider s being Variable such that

A22: ( ( z = y & s = x ) or ( z <> y & s = z ) ) ;

assume A23: not x in variables_in (All (z,H)) ; :: thesis: for v being Function of VAR,M holds

( M,v |= (All (z,H)) / (y,x) iff M,v / (y,(v . x)) |= All (z,H) )

then A24: not x in (variables_in H) \/ {z} by ZF_LANG1:142;

then not x in {z} by XBOOLE_0:def 3;

then A25: x <> z by TARSKI:def 1;

let v be Function of VAR,M; :: thesis: ( M,v |= (All (z,H)) / (y,x) iff M,v / (y,(v . x)) |= All (z,H) )

Free H c= variables_in H by ZF_LANG1:151;

then A26: not x in Free H by A24, XBOOLE_0:def 3;

thus ( M,v |= (All (z,H)) / (y,x) implies M,v / (y,(v . x)) |= All (z,H) ) :: thesis: ( M,v / (y,(v . x)) |= All (z,H) implies M,v |= (All (z,H)) / (y,x) )

Free (All (z,H)) c= variables_in (All (z,H)) by ZF_LANG1:151;

then A38: not x in Free (All (z,H)) by A23;

end;S

let z be Variable; :: thesis: ( S

assume A21: ( not x in variables_in H implies for v being Function of VAR,M holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: S

( z = y or z <> y ) ;

then consider s being Variable such that

A22: ( ( z = y & s = x ) or ( z <> y & s = z ) ) ;

assume A23: not x in variables_in (All (z,H)) ; :: thesis: for v being Function of VAR,M holds

( M,v |= (All (z,H)) / (y,x) iff M,v / (y,(v . x)) |= All (z,H) )

then A24: not x in (variables_in H) \/ {z} by ZF_LANG1:142;

then not x in {z} by XBOOLE_0:def 3;

then A25: x <> z by TARSKI:def 1;

let v be Function of VAR,M; :: thesis: ( M,v |= (All (z,H)) / (y,x) iff M,v / (y,(v . x)) |= All (z,H) )

Free H c= variables_in H by ZF_LANG1:151;

then A26: not x in Free H by A24, XBOOLE_0:def 3;

thus ( M,v |= (All (z,H)) / (y,x) implies M,v / (y,(v . x)) |= All (z,H) ) :: thesis: ( M,v / (y,(v . x)) |= All (z,H) implies M,v |= (All (z,H)) / (y,x) )

proof

assume A37:
M,v / (y,(v . x)) |= All (z,H)
; :: thesis: M,v |= (All (z,H)) / (y,x)
assume
M,v |= (All (z,H)) / (y,x)
; :: thesis: M,v / (y,(v . x)) |= All (z,H)

then A27: M,v |= All (s,(H / (y,x))) by A22, ZF_LANG1:159, ZF_LANG1:160;

end;then A27: M,v |= All (s,(H / (y,x))) by A22, ZF_LANG1:159, ZF_LANG1:160;

A28: now :: thesis: ( z = y & s = x implies M,v / (y,(v . x)) |= All (z,H) )

assume that

A29: z = y and

A30: s = x ; :: thesis: M,v / (y,(v . x)) |= All (z,H)

hence M,v / (y,(v . x)) |= All (z,H) by A29, ZF_LANG1:72; :: thesis: verum

end;A29: z = y and

A30: s = x ; :: thesis: M,v / (y,(v . x)) |= All (z,H)

now :: thesis: for m being Element of M holds M,v / (y,m) |= H

then
M,v |= All (y,H)
by ZF_LANG1:71;let m be Element of M; :: thesis: M,v / (y,m) |= H

A31: (v / (x,m)) . x = m by FUNCT_7:128;

M,v / (x,m) |= H / (y,x) by A27, A30, ZF_LANG1:71;

then A32: M,(v / (x,m)) / (y,((v / (x,m)) . x)) |= H by A21, A24, XBOOLE_0:def 3;

(v / (x,m)) / (y,m) = (v / (y,m)) / (x,m) by A25, A29, FUNCT_7:33;

then M,(v / (y,m)) / (x,m) |= All (x,H) by A26, A32, A31, ZFMODEL1:10;

then A33: M,((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)) |= H by ZF_LANG1:71;

((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)) = (v / (y,m)) / (x,((v / (y,m)) . x)) by FUNCT_7:34;

hence M,v / (y,m) |= H by A33, FUNCT_7:35; :: thesis: verum

end;A31: (v / (x,m)) . x = m by FUNCT_7:128;

M,v / (x,m) |= H / (y,x) by A27, A30, ZF_LANG1:71;

then A32: M,(v / (x,m)) / (y,((v / (x,m)) . x)) |= H by A21, A24, XBOOLE_0:def 3;

(v / (x,m)) / (y,m) = (v / (y,m)) / (x,m) by A25, A29, FUNCT_7:33;

then M,(v / (y,m)) / (x,m) |= All (x,H) by A26, A32, A31, ZFMODEL1:10;

then A33: M,((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)) |= H by ZF_LANG1:71;

((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)) = (v / (y,m)) / (x,((v / (y,m)) . x)) by FUNCT_7:34;

hence M,v / (y,m) |= H by A33, FUNCT_7:35; :: thesis: verum

hence M,v / (y,(v . x)) |= All (z,H) by A29, ZF_LANG1:72; :: thesis: verum

now :: thesis: ( z <> y & s = z implies M,v / (y,(v . x)) |= All (z,H) )

hence
M,v / (y,(v . x)) |= All (z,H)
by A22, A28; :: thesis: verumassume that

A34: z <> y and

A35: s = z ; :: thesis: M,v / (y,(v . x)) |= All (z,H)

end;A34: z <> y and

A35: s = z ; :: thesis: M,v / (y,(v . x)) |= All (z,H)

now :: thesis: for m being Element of M holds M,(v / (y,(v . x))) / (z,m) |= H

hence
M,v / (y,(v . x)) |= All (z,H)
by ZF_LANG1:71; :: thesis: verumlet m be Element of M; :: thesis: M,(v / (y,(v . x))) / (z,m) |= H

M,v / (z,m) |= H / (y,x) by A27, A35, ZF_LANG1:71;

then A36: M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by A21, A24, XBOOLE_0:def 3;

(v / (z,m)) . x = v . x by A25, FUNCT_7:32;

hence M,(v / (y,(v . x))) / (z,m) |= H by A34, A36, FUNCT_7:33; :: thesis: verum

end;M,v / (z,m) |= H / (y,x) by A27, A35, ZF_LANG1:71;

then A36: M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by A21, A24, XBOOLE_0:def 3;

(v / (z,m)) . x = v . x by A25, FUNCT_7:32;

hence M,(v / (y,(v . x))) / (z,m) |= H by A34, A36, FUNCT_7:33; :: thesis: verum

Free (All (z,H)) c= variables_in (All (z,H)) by ZF_LANG1:151;

then A38: not x in Free (All (z,H)) by A23;

A39: now :: thesis: ( z = y & s = x implies M,v |= (All (z,H)) / (y,x) )

assume that

A40: z = y and

s = x ; :: thesis: M,v |= (All (z,H)) / (y,x)

M,v |= All (y,H) by A37, A40, ZF_LANG1:72;

then A41: M,v |= All (x,(All (y,H))) by A38, A40, ZFMODEL1:10;

hence M,v |= (All (z,H)) / (y,x) by A40, ZF_LANG1:160; :: thesis: verum

end;A40: z = y and

s = x ; :: thesis: M,v |= (All (z,H)) / (y,x)

M,v |= All (y,H) by A37, A40, ZF_LANG1:72;

then A41: M,v |= All (x,(All (y,H))) by A38, A40, ZFMODEL1:10;

now :: thesis: for m being Element of M holds M,v / (x,m) |= H / (y,x)

then
M,v |= All (x,(H / (y,x)))
by ZF_LANG1:71;let m be Element of M; :: thesis: M,v / (x,m) |= H / (y,x)

M,v / (x,m) |= All (y,H) by A41, ZF_LANG1:71;

then A42: M,(v / (x,m)) / (y,m) |= H by ZF_LANG1:71;

(v / (x,m)) . x = m by FUNCT_7:128;

hence M,v / (x,m) |= H / (y,x) by A21, A24, A42, XBOOLE_0:def 3; :: thesis: verum

end;M,v / (x,m) |= All (y,H) by A41, ZF_LANG1:71;

then A42: M,(v / (x,m)) / (y,m) |= H by ZF_LANG1:71;

(v / (x,m)) . x = m by FUNCT_7:128;

hence M,v / (x,m) |= H / (y,x) by A21, A24, A42, XBOOLE_0:def 3; :: thesis: verum

hence M,v |= (All (z,H)) / (y,x) by A40, ZF_LANG1:160; :: thesis: verum

now :: thesis: ( z <> y & s = z implies M,v |= (All (z,H)) / (y,x) )

hence
M,v |= (All (z,H)) / (y,x)
by A22, A39; :: thesis: verumassume that

A43: z <> y and

s = z ; :: thesis: M,v |= (All (z,H)) / (y,x)

hence M,v |= (All (z,H)) / (y,x) by A43, ZF_LANG1:159; :: thesis: verum

end;A43: z <> y and

s = z ; :: thesis: M,v |= (All (z,H)) / (y,x)

now :: thesis: for m being Element of M holds M,v / (z,m) |= H / (y,x)

then
M,v |= All (z,(H / (y,x)))
by ZF_LANG1:71;let m be Element of M; :: thesis: M,v / (z,m) |= H / (y,x)

M,(v / (y,(v . x))) / (z,m) |= H by A37, ZF_LANG1:71;

then M,(v / (z,m)) / (y,(v . x)) |= H by A43, FUNCT_7:33;

then M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by A25, FUNCT_7:32;

hence M,v / (z,m) |= H / (y,x) by A21, A24, XBOOLE_0:def 3; :: thesis: verum

end;M,(v / (y,(v . x))) / (z,m) |= H by A37, ZF_LANG1:71;

then M,(v / (z,m)) / (y,(v . x)) |= H by A43, FUNCT_7:33;

then M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by A25, FUNCT_7:32;

hence M,v / (z,m) |= H / (y,x) by A21, A24, XBOOLE_0:def 3; :: thesis: verum

hence M,v |= (All (z,H)) / (y,x) by A43, ZF_LANG1:159; :: thesis: verum

S

proof

for H being ZF-formula holds S
let H be ZF-formula; :: thesis: ( S_{1}[H] implies S_{1}[ 'not' H] )

assume A45: ( not x in variables_in H implies for v being Function of VAR,M holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: S_{1}[ 'not' H]

assume A46: not x in variables_in ('not' H) ; :: thesis: for v being Function of VAR,M holds

( M,v |= ('not' H) / (y,x) iff M,v / (y,(v . x)) |= 'not' H )

let v be Function of VAR,M; :: thesis: ( M,v |= ('not' H) / (y,x) iff M,v / (y,(v . x)) |= 'not' H )

thus ( M,v |= ('not' H) / (y,x) implies M,v / (y,(v . x)) |= 'not' H ) :: thesis: ( M,v / (y,(v . x)) |= 'not' H implies M,v |= ('not' H) / (y,x) )

then not M,v / (y,(v . x)) |= H by ZF_MODEL:14;

then not M,v |= H / (y,x) by A45, A46, ZF_LANG1:140;

then M,v |= 'not' (H / (y,x)) by ZF_MODEL:14;

hence M,v |= ('not' H) / (y,x) by ZF_LANG1:156; :: thesis: verum

end;assume A45: ( not x in variables_in H implies for v being Function of VAR,M holds

( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: S

assume A46: not x in variables_in ('not' H) ; :: thesis: for v being Function of VAR,M holds

( M,v |= ('not' H) / (y,x) iff M,v / (y,(v . x)) |= 'not' H )

let v be Function of VAR,M; :: thesis: ( M,v |= ('not' H) / (y,x) iff M,v / (y,(v . x)) |= 'not' H )

thus ( M,v |= ('not' H) / (y,x) implies M,v / (y,(v . x)) |= 'not' H ) :: thesis: ( M,v / (y,(v . x)) |= 'not' H implies M,v |= ('not' H) / (y,x) )

proof

assume
M,v / (y,(v . x)) |= 'not' H
; :: thesis: M,v |= ('not' H) / (y,x)
assume
M,v |= ('not' H) / (y,x)
; :: thesis: M,v / (y,(v . x)) |= 'not' H

then M,v |= 'not' (H / (y,x)) by ZF_LANG1:156;

then not M,v |= H / (y,x) by ZF_MODEL:14;

then not M,v / (y,(v . x)) |= H by A45, A46, ZF_LANG1:140;

hence M,v / (y,(v . x)) |= 'not' H by ZF_MODEL:14; :: thesis: verum

end;then M,v |= 'not' (H / (y,x)) by ZF_LANG1:156;

then not M,v |= H / (y,x) by ZF_MODEL:14;

then not M,v / (y,(v . x)) |= H by A45, A46, ZF_LANG1:140;

hence M,v / (y,(v . x)) |= 'not' H by ZF_MODEL:14; :: thesis: verum

then not M,v / (y,(v . x)) |= H by ZF_MODEL:14;

then not M,v |= H / (y,x) by A45, A46, ZF_LANG1:140;

then M,v |= 'not' (H / (y,x)) by ZF_MODEL:14;

hence M,v |= ('not' H) / (y,x) by ZF_LANG1:156; :: thesis: verum

hence ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; :: thesis: verum