let X be set ; :: thesis: for W being Universe st omega in W & X in W holds

ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF )

let W be Universe; :: thesis: ( omega in W & X in W implies ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF ) )

assume A1: omega in W ; :: thesis: ( not X in W or ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF ) )

A2: W = Rank (On W) by CLASSES2:50;

assume X in W ; :: thesis: ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF )

then the_rank_of X in the_rank_of W by CLASSES1:68;

then the_rank_of X in On W by A2, CLASSES1:64;

then reconsider a = the_rank_of X as Ordinal of W by ZF_REFLE:7;

consider b being Ordinal of W, M being non empty set such that

A3: a in b and

A4: M = Rank b and

A5: M <==> W by A1, Th38;

take M ; :: thesis: ( X in M & M in W & M is being_a_model_of_ZF )

X c= Rank a by CLASSES1:def 9;

then A6: X in Rank (succ a) by CLASSES1:32;

succ a c= b by A3, ORDINAL1:21;

then Rank (succ a) c= M by A4, CLASSES1:37;

hence X in M by A6; :: thesis: ( M in W & M is being_a_model_of_ZF )

b in On W by ZF_REFLE:7;

hence M in W by A2, A4, CLASSES1:36; :: thesis: M is being_a_model_of_ZF

W is being_a_model_of_ZF by A1, ZF_REFLE:6;

then W |= ZF-axioms by Th4;

then M |= ZF-axioms by A5, Th8;

hence M is being_a_model_of_ZF by A4, Th5; :: thesis: verum

ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF )

let W be Universe; :: thesis: ( omega in W & X in W implies ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF ) )

assume A1: omega in W ; :: thesis: ( not X in W or ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF ) )

A2: W = Rank (On W) by CLASSES2:50;

assume X in W ; :: thesis: ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF )

then the_rank_of X in the_rank_of W by CLASSES1:68;

then the_rank_of X in On W by A2, CLASSES1:64;

then reconsider a = the_rank_of X as Ordinal of W by ZF_REFLE:7;

consider b being Ordinal of W, M being non empty set such that

A3: a in b and

A4: M = Rank b and

A5: M <==> W by A1, Th38;

take M ; :: thesis: ( X in M & M in W & M is being_a_model_of_ZF )

X c= Rank a by CLASSES1:def 9;

then A6: X in Rank (succ a) by CLASSES1:32;

succ a c= b by A3, ORDINAL1:21;

then Rank (succ a) c= M by A4, CLASSES1:37;

hence X in M by A6; :: thesis: ( M in W & M is being_a_model_of_ZF )

b in On W by ZF_REFLE:7;

hence M in W by A2, A4, CLASSES1:36; :: thesis: M is being_a_model_of_ZF

W is being_a_model_of_ZF by A1, ZF_REFLE:6;

then W |= ZF-axioms by Th4;

then M |= ZF-axioms by A5, Th8;

hence M is being_a_model_of_ZF by A4, Th5; :: thesis: verum