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_{1} being M8( omega ) holds

( not {(x. 0),(x. 1),(x. 2)} misses Free b_{1} or M |= the_axiom_of_substitution_for b_{1} )

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

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

( not {(x. 0),(x. 1),(x. 2)} misses Free 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