let H be ZF-formula; 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; 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 ; 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; 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; ( M,v |= All (x,H) iff M,v / (x,m) |= All (x,H) )
A1:
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;
for m being Element of M st M,v |= All (x,H) holds
M,v / (x,m) |= All (x,H)let m be
Element of
M;
( M,v |= All (x,H) implies M,v / (x,m) |= All (x,H) )
assume A2:
M,
v |= All (
x,
H)
;
M,v / (x,m) |= All (x,H)
now for m9 being Element of M holds M,(v / (x,m)) / (x,m9) |= Hlet m9 be
Element of
M;
M,(v / (x,m)) / (x,m9) |= H
(v / (x,m)) / (
x,
m9)
= v / (
x,
m9)
by FUNCT_7:34;
hence
M,
(v / (x,m)) / (
x,
m9)
|= H
by A2, Th71;
verum end;
hence
M,
v / (
x,
m)
|= All (
x,
H)
by Th71;
verum
end;
(v / (x,m)) / (x,(v . x)) =
v / (x,(v . x))
by FUNCT_7:34
.=
v
by FUNCT_7:35
;
hence
( M,v |= All (x,H) iff M,v / (x,m) |= All (x,H) )
by A1; verum