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 ) )
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 A2: ( the_rank_of X in the_rank_of W & W = Rank (On W) ) by CLASSES1:76, CLASSES2:54;
then the_rank_of X in On W by CLASSES1:72;
then reconsider a = the_rank_of X as Ordinal of W by ZF_REFLE:8;
consider b being Ordinal of W, M being non empty set such that
A3: ( a in b & M = Rank b & M <==> W ) by A1, Th40;
take M ; :: thesis: ( X in M & M in W & M is being_a_model_of_ZF )
( X c= Rank a & succ a c= b ) by A3, CLASSES1:def 8, ORDINAL1:33;
then ( X in Rank (succ a) & Rank (succ a) c= M ) by A3, CLASSES1:36, CLASSES1:43;
hence X in M ; :: thesis: ( M in W & M is being_a_model_of_ZF )
b in On W by ZF_REFLE:8;
hence M in W by A2, A3, CLASSES1:42; :: thesis: M is being_a_model_of_ZF
W is being_a_model_of_ZF by A1, ZF_REFLE:7;
then W |= ZF-axioms by Th4;
then ( M |= ZF-axioms & M is epsilon-transitive ) by A3, Th8;
hence M is being_a_model_of_ZF by Th5; :: thesis: verum