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