let W be Universe; :: thesis: for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H
for H being ZF-formula
for f being Function of VAR ,W st {(x. 0 ),(x. 1),(x. 2)} misses Free H & W,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for u being Element of W holds (def_func' H,f) .: u in W
proof
let H be
ZF-formula;
:: thesis: for f being Function of VAR ,W st {(x. 0 ),(x. 1),(x. 2)} misses Free H & W,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for u being Element of W holds (def_func' H,f) .: u in Wlet f be
Function of
VAR ,
W;
:: thesis: ( {(x. 0 ),(x. 1),(x. 2)} misses Free H & W,f |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) implies for u being Element of W holds (def_func' H,f) .: u in W )
assume
(
{(x. 0 ),(x. 1),(x. 2)} misses Free H &
W,
f |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) )
;
:: thesis: for u being Element of W holds (def_func' H,f) .: u in W
let u be
Element of
W;
:: thesis: (def_func' H,f) .: u in W
(
card u in card W &
(def_func' H,f) .: u c= W &
card ((def_func' H,f) .: u) c= card u )
by CARD_2:3, CLASSES2:1;
then
card ((def_func' H,f) .: u) in card W
by ORDINAL1:22;
hence
(def_func' H,f) .: u in W
by CLASSES1:2;
:: thesis: verum
end;
hence
for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H
by ZFMODEL1:19; :: thesis: verum