let M be non empty set ; :: thesis: ( M |= ZF-axioms & M is epsilon-transitive implies M is being_a_model_of_ZF )
the_axiom_of_power_sets in WFF by ZF_LANG:4;
then A1: the_axiom_of_power_sets in ZF-axioms by Def4;
the_axiom_of_infinity in WFF by ZF_LANG:4;
then A2: the_axiom_of_infinity in ZF-axioms by Def4;
the_axiom_of_unions in WFF by ZF_LANG:4;
then A3: the_axiom_of_unions in ZF-axioms by Def4;
assume that
A4: for H being ZF-formula st H in ZF-axioms holds
M |= H and
A5: M is epsilon-transitive ; :: according to ZFREFLE1:def 1 :: thesis: M is being_a_model_of_ZF
the_axiom_of_pairs in WFF by ZF_LANG:4;
then the_axiom_of_pairs 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 A4, A5, A3, A2, A1; :: according to ZF_MODEL:def 12 :: thesis: for b₁ being M8( omega ) 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 )
assume A6: {(x. 0),(x. 1),(x. 2)} misses Free H ; :: thesis: M |= the_axiom_of_substitution_for H
the_axiom_of_substitution_for H in WFF by ZF_LANG:4;
then the_axiom_of_substitution_for H in ZF-axioms by A6, Def4;
hence M |= the_axiom_of_substitution_for H by A4; :: thesis: verum