begin
set x0 = x. 0;
set x1 = x. 1;
set x2 = x. 2;
set x3 = x. 3;
set x4 = x. 4;
defpred S1[ Nat] means for x being Variable
for E being non empty set
for H being ZF-formula
for f being Function of VAR,E st len H = $1 & not x in Free H & E,f |= H holds
E,f |= All (x,H);
Lm1:
for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
Lm2:
for x being Variable
for H being ZF-formula holds
( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x )
theorem
for
x,
y,
z being
Variable for
H being
ZF-formula for
E being non
empty set for
f being
Function of
VAR,
E st
{x,y,z} misses Free H &
E,
f |= H holds
E,
f |= All (
x,
y,
z,
H)
definition
let H be
ZF-formula;
let E be non
empty set ;
let val be
Function of
VAR,
E;
assume that A1:
not
x. 0 in Free H
and A2:
E,
val |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
;
existence
ex b1 being Function of E,E st
for g being Function of VAR,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) )
uniqueness
for b1, b2 being Function of E,E st ( for g being Function of VAR,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff b2 . (g . (x. 3)) = g . (x. 4) ) ) holds
b1 = b2
end;
definition
let H be
ZF-formula;
let E be non
empty set ;
assume that A1:
Free H c= {(x. 3),(x. 4)}
and A2:
E |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
;
existence
ex b1 being Function of E,E st
for g being Function of VAR,E holds
( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) )
uniqueness
for b1, b2 being Function of E,E st ( for g being Function of VAR,E holds
( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E holds
( E,g |= H iff b2 . (g . (x. 3)) = g . (x. 4) ) ) holds
b1 = b2
end;
theorem Th15:
for
E being non
empty set st
E is
epsilon-transitive holds
( ( for
H being
ZF-formula st
{(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for
H being
ZF-formula for
f being
Function of
VAR,
E st
{(x. 0),(x. 1),(x. 2)} misses Free H &
E,
f |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for
u being
Element of
E holds
(def_func' (H,f)) .: u in E )
Lm3:
for E being non empty set st E is epsilon-transitive holds
for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v
theorem
for
E being non
empty set st
E is
being_a_model_of_ZF holds
(
E is
epsilon-transitive & ( for
u,
v being
Element of
E st ( for
w being
Element of
E holds
(
w in u iff
w in v ) ) holds
u = v ) & ( for
u,
v being
Element of
E holds
{u,v} in E ) & ( for
u being
Element of
E holds
union u in E ) & ex
u being
Element of
E st
(
u <> {} & ( for
v being
Element of
E st
v in u holds
ex
w being
Element of
E st
(
v c< w &
w in u ) ) ) & ( for
u being
Element of
E holds
E /\ (bool u) in E ) & ( for
H being
ZF-formula for
f being
Function of
VAR,
E st
{(x. 0),(x. 1),(x. 2)} misses Free H &
E,
f |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for
u being
Element of
E holds
(def_func' (H,f)) .: u in E ) )
theorem
for
E being non
empty set st
E is
epsilon-transitive & ( for
u,
v being
Element of
E holds
{u,v} in E ) & ( for
u being
Element of
E holds
union u in E ) & ex
u being
Element of
E st
(
u <> {} & ( for
v being
Element of
E st
v in u holds
ex
w being
Element of
E st
(
v c< w &
w in u ) ) ) & ( for
u being
Element of
E holds
E /\ (bool u) in E ) & ( for
H being
ZF-formula for
f being
Function of
VAR,
E st
{(x. 0),(x. 1),(x. 2)} misses Free H &
E,
f |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for
u being
Element of
E holds
(def_func' (H,f)) .: u in E ) holds
E is
being_a_model_of_ZF