let x, y be Variable; 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 ; 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; 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; ( not x in variables_in H implies ( M,v |= H / y,x iff M,v / y,(v . x) |= H ) )
defpred S1[ 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
( S1[x1 '=' x2] & S1[x1 'in' x2] )
proof
let x1,
x2 be
Variable;
( S1[x1 '=' x2] & S1[x1 'in' x2] )
A2:
(
x2 = y or
x2 <> y )
;
A3:
(
x1 = y or
x1 <> y )
;
thus
S1[
x1 '=' x2]
S1[x1 'in' x2]proof
assume
not
x in variables_in (x1 '=' x2)
;
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;
( 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:34, FUNCT_7:130;
A6:
(v / y,(v . x)) . x1 = v . y1
by A4, FUNCT_7:34, FUNCT_7:130;
A7:
(x1 '=' x2) / y,
x = y1 '=' y2
by A4, ZF_LANG1:166;
thus
(
M,
v |= (x1 '=' x2) / y,
x implies
M,
v / y,
(v . x) |= x1 '=' x2 )
( M,v / y,(v . x) |= x1 '=' x2 implies M,v |= (x1 '=' x2) / y,x )
assume
M,
v / y,
(v . x) |= x1 '=' x2
;
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;
verum
end;
consider y1,
y2 being
Variable such that 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)
;
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;
( 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:34, FUNCT_7:130;
A10:
(v / y,(v . x)) . x2 = v . y2
by A8, FUNCT_7:34, FUNCT_7:130;
A11:
(x1 'in' x2) / y,
x = y1 'in' y2
by A8, ZF_LANG1:168;
thus
(
M,
v |= (x1 'in' x2) / y,
x implies
M,
v / y,
(v . x) |= x1 'in' x2 )
( M,v / y,(v . x) |= x1 'in' x2 implies M,v |= (x1 'in' x2) / y,x )
assume
M,
v / y,
(v . x) |= x1 'in' x2
;
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;
verum
end;
A12:
for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1,
H2 be
ZF-formula;
( S1[H1] & S1[H2] implies S1[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 ) )
;
S1[H1 '&' H2]
assume
not
x in variables_in (H1 '&' H2)
;
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:154;
let v be
Function of
VAR ,
M;
( 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 )
( M,v / y,(v . x) |= H1 '&' H2 implies M,v |= (H1 '&' H2) / y,x )proof
assume
M,
v |= (H1 '&' H2) / y,
x
;
M,v / y,(v . x) |= H1 '&' H2
then A16:
M,
v |= (H1 / y,x) '&' (H2 / y,x)
by ZF_LANG1:172;
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;
verum
end;
assume A18:
M,
v / y,
(v . x) |= H1 '&' H2
;
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:172;
verum
end;
A20:
for H being ZF-formula
for z being Variable st S1[H] holds
S1[ All z,H]
proof
let H be
ZF-formula;
for z being Variable st S1[H] holds
S1[ All z,H]let z be
Variable;
( S1[H] implies S1[ 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 ) )
;
S1[ 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)
;
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:155;
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;
( 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:164;
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 )
( M,v / y,(v . x) |= All z,H implies M,v |= (All z,H) / y,x )proof
assume
M,
v |= (All z,H) / y,
x
;
M,v / y,(v . x) |= All z,H
then A27:
M,
v |= All s,
(H / y,x)
by A22, ZF_LANG1:173, ZF_LANG1:174;
A28:
now assume that A29:
z = y
and A30:
s = x
;
M,v / y,(v . x) |= All z,Hnow let m be
Element of
M;
M,v / y,m |= HA31:
(v / x,m) . x = m
by FUNCT_7:130;
M,
v / x,
m |= H / y,
x
by A27, A30, ZF_LANG1:80;
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:35;
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:80;
((v / y,m) / x,m) / x,
((v / y,m) . x) = (v / y,m) / x,
((v / y,m) . x)
by FUNCT_7:36;
hence
M,
v / y,
m |= H
by A33, FUNCT_7:37;
verum end; then
M,
v |= All y,
H
by ZF_LANG1:80;
hence
M,
v / y,
(v . x) |= All z,
H
by A29, ZF_LANG1:81;
verum end;
now assume that A34:
z <> y
and A35:
s = z
;
M,v / y,(v . x) |= All z,Hnow let m be
Element of
M;
M,(v / y,(v . x)) / z,m |= H
M,
v / z,
m |= H / y,
x
by A27, A35, ZF_LANG1:80;
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:34;
hence
M,
(v / y,(v . x)) / z,
m |= H
by A34, A36, FUNCT_7:35;
verum end; hence
M,
v / y,
(v . x) |= All z,
H
by ZF_LANG1:80;
verum end;
hence
M,
v / y,
(v . x) |= All z,
H
by A22, A28;
verum
end;
assume A37:
M,
v / y,
(v . x) |= All z,
H
;
M,v |= (All z,H) / y,x
Free (All z,H) c= variables_in (All z,H)
by ZF_LANG1:164;
then A38:
not
x in Free (All z,H)
by A23;
A39:
now assume that A40:
z = y
and
s = x
;
M,v |= (All z,H) / y,x
M,
v |= All y,
H
by A37, A40, ZF_LANG1:81;
then A41:
M,
v |= All x,
(All y,H)
by A38, A40, ZFMODEL1:10;
now let m be
Element of
M;
M,v / x,m |= H / y,x
M,
v / x,
m |= All y,
H
by A41, ZF_LANG1:80;
then A42:
M,
(v / x,m) / y,
m |= H
by ZF_LANG1:80;
(v / x,m) . x = m
by FUNCT_7:130;
hence
M,
v / x,
m |= H / y,
x
by A21, A24, A42, XBOOLE_0:def 3;
verum end; then
M,
v |= All x,
(H / y,x)
by ZF_LANG1:80;
hence
M,
v |= (All z,H) / y,
x
by A40, ZF_LANG1:174;
verum end;
now assume that A43:
z <> y
and
s = z
;
M,v |= (All z,H) / y,xnow let m be
Element of
M;
M,v / z,m |= H / y,x
M,
(v / y,(v . x)) / z,
m |= H
by A37, ZF_LANG1:80;
then
M,
(v / z,m) / y,
(v . x) |= H
by A43, FUNCT_7:35;
then
M,
(v / z,m) / y,
((v / z,m) . x) |= H
by A25, FUNCT_7:34;
hence
M,
v / z,
m |= H / y,
x
by A21, A24, XBOOLE_0:def 3;
verum end; then
M,
v |= All z,
(H / y,x)
by ZF_LANG1:80;
hence
M,
v |= (All z,H) / y,
x
by A43, ZF_LANG1:173;
verum end;
hence
M,
v |= (All z,H) / y,
x
by A22, A39;
verum
end;
A44:
for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be
ZF-formula;
( S1[H] implies S1[ '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 ) )
;
S1[ 'not' H]
assume A46:
not
x in variables_in ('not' H)
;
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;
( 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 )
( M,v / y,(v . x) |= 'not' H implies M,v |= ('not' H) / y,x )proof
assume
M,
v |= ('not' H) / y,
x
;
M,v / y,(v . x) |= 'not' H
then
M,
v |= 'not' (H / y,x)
by ZF_LANG1:170;
then
not
M,
v |= H / y,
x
by ZF_MODEL:14;
then
not
M,
v / y,
(v . x) |= H
by A45, A46, ZF_LANG1:153;
hence
M,
v / y,
(v . x) |= 'not' H
by ZF_MODEL:14;
verum
end;
assume
M,
v / y,
(v . x) |= 'not' H
;
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:153;
then
M,
v |= 'not' (H / y,x)
by ZF_MODEL:14;
hence
M,
v |= ('not' H) / y,
x
by ZF_LANG1:170;
verum
end;
for H being ZF-formula holds S1[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 ) )
; verum