let M be non empty set ; :: thesis: ( M |= ZF-axioms & M is epsilon-transitive implies M is being_a_model_of_ZF )
assume that
A1: for H being ZF-formula st H in ZF-axioms holds
M |= H and
A2: M is epsilon-transitive ; :: according to ZFREFLE1:def 1 :: thesis: M is being_a_model_of_ZF
( the_axiom_of_pairs in WFF & the_axiom_of_unions in WFF & the_axiom_of_infinity in WFF & the_axiom_of_power_sets in WFF ) by ZF_LANG:14;
then ( the_axiom_of_pairs in ZF-axioms & the_axiom_of_unions in ZF-axioms & the_axiom_of_infinity in ZF-axioms & the_axiom_of_power_sets in ZF-axioms ) by Def4;
hence ( M is epsilon-transitive & M |= the_axiom_of_pairs & M |= the_axiom_of_unions & M |= the_axiom_of_infinity & M |= the_axiom_of_power_sets ) by A1, A2; :: according to ZF_MODEL:def 12 :: thesis: for b₁ being M7( NAT ) holds
( not {(x. 0 ),(x. 1),(x. 2)} misses Free b₁ or M |= the_axiom_of_substitution_for b₁ )
let H be ZF-formula; :: thesis: ( not {(x. 0 ),(x. 1),(x. 2)} misses Free H or M |= the_axiom_of_substitution_for H )
A3: the_axiom_of_substitution_for H in WFF by ZF_LANG:14;
assume {(x. 0 ),(x. 1),(x. 2)} misses Free H ; :: thesis: M |= the_axiom_of_substitution_for H
then the_axiom_of_substitution_for H in ZF-axioms by A3, Def4;
hence M |= the_axiom_of_substitution_for H by A1; :: thesis: verum