let H be ZF-formula; :: thesis: for x being Variable
for M being non empty set
for m being Element of M
for v being Function of VAR ,M holds
( M,v |= All x,H iff M,v / x,m |= All x,H )
let x be Variable; :: thesis: for M being non empty set
for m being Element of M
for v being Function of VAR ,M holds
( M,v |= All x,H iff M,v / x,m |= All x,H )
let M be non empty set ; :: thesis: for m being Element of M
for v being Function of VAR ,M holds
( M,v |= All x,H iff M,v / x,m |= All x,H )
let m be Element of M; :: thesis: for v being Function of VAR ,M holds
( M,v |= All x,H iff M,v / x,m |= All x,H )
let v be Function of VAR ,M; :: thesis: ( M,v |= All x,H iff M,v / x,m |= All x,H )
A1: (v / x,m) / x,(v . x) =
v / x,(v . x)
by FUNCT_7:36
.=
v
by FUNCT_7:37
;
for v being Function of VAR ,M
for m being Element of M st M,v |= All x,H holds
M,v / x,m |= All x,H
proof
let v be
Function of
VAR ,
M;
:: thesis: for m being Element of M st M,v |= All x,H holds
M,v / x,m |= All x,Hlet m be
Element of
M;
:: thesis: ( M,v |= All x,H implies M,v / x,m |= All x,H )
assume A2:
M,
v |= All x,
H
;
:: thesis: M,v / x,m |= All x,H
now let m' be
Element of
M;
:: thesis: M,(v / x,m) / x,m' |= H
(v / x,m) / x,
m' = v / x,
m'
by FUNCT_7:36;
hence
M,
(v / x,m) / x,
m' |= H
by A2, Th80;
:: thesis: verum end;
hence
M,
v / x,
m |= All x,
H
by Th80;
:: thesis: verum
end;
hence
( M,v |= All x,H iff M,v / x,m |= All x,H )
by A1; :: thesis: verum