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:54;
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:76;
then the_rank_of X in On W by A2, 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 and
A4: M = Rank b and
A5: 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 by CLASSES1:def 8;
then A6: X in Rank (succ a) by CLASSES1:36;
succ a c= b by A3, ORDINAL1:33;
then Rank (succ a) c= M by A4, CLASSES1:43;
hence X in M by A6; :: 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, A4, 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 by A5, Th8;
hence M is being_a_model_of_ZF by A4, Th5; :: thesis: verum