let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( ( 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 F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ) )
assume A1:
E is epsilon-transitive
; :: thesis: ( ( 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 F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E )
thus
( ( for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) implies for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E )
:: thesis: ( ( for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ) implies for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H )proof
assume A2:
for
H being
ZF-formula st
{(x. 0 ),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H
;
:: thesis: for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E
let F be
Function;
:: thesis: ( F is_parametrically_definable_in E implies for X being set st X in E holds
F .: X in E )
given H being
ZF-formula,
f being
Function of
VAR ,
E such that A3:
{(x. 0 ),(x. 1),(x. 2)} misses Free H
and A4:
E,
f |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))))
and A5:
F = def_func' H,
f
;
:: according to ZFMODEL1:def 4 :: thesis: for X being set st X in E holds
F .: X in E
let X be
set ;
:: thesis: ( X in E implies F .: X in E )
assume
X in E
;
:: thesis: F .: X in E
then reconsider u =
X as
Element of
E ;
(def_func' H,f) .: u in E
by A1, A2, A3, A4, Th19;
hence
F .: X in E
by A5;
:: thesis: verum
end;
assume A6:
for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E
; :: thesis: for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H
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
proof
let H be
ZF-formula;
:: thesis: 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 Elet f be
Function of
VAR ,
E;
:: thesis: ( {(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 ))))) implies for u being Element of E holds (def_func' H,f) .: u in E )
assume that A7:
{(x. 0 ),(x. 1),(x. 2)} misses Free H
and A8:
E,
f |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))))
;
:: thesis: for u being Element of E holds (def_func' H,f) .: u in E
A9:
def_func' H,
f is_parametrically_definable_in E
by A7, A8, Def4;
let u be
Element of
E;
:: thesis: (def_func' H,f) .: u in E
thus
(def_func' H,f) .: u in E
by A6, A9;
:: thesis: verum
end;
hence
for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H
by A1, Th19; :: thesis: verum