let X be set ; :: thesis: for A being Ordinal holds
( A c= the_rank_of X iff for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) )
let A be Ordinal; :: thesis: ( A c= the_rank_of X iff for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) )
thus ( A c= the_rank_of X implies for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ) :: thesis: ( ( for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ) implies A c= the_rank_of X )
proof
assume A1: A c= the_rank_of X ; :: thesis: for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y )
let B be Ordinal; :: thesis: ( B in A implies ex Y being set st
( Y in X & B c= the_rank_of Y ) )
assume B in A ; :: thesis: ex Y being set st
( Y in X & B c= the_rank_of Y )
then not the_rank_of X c= B by A1, ORDINAL1:5;
then not X c= Rank B by Def9;
then A2: X \ (Rank B) <> {} by XBOOLE_1:37;
set x = the Element of X \ (Rank B);
take the Element of X \ (Rank B) ; :: thesis: ( the Element of X \ (Rank B) in X & B c= the_rank_of the Element of X \ (Rank B) )
A3: not the Element of X \ (Rank B) in Rank B by A2, XBOOLE_0:def 5;
thus the Element of X \ (Rank B) in X by A2, XBOOLE_0:def 5; :: thesis: B c= the_rank_of the Element of X \ (Rank B)
thus B c= the_rank_of the Element of X \ (Rank B) by ORDINAL1:16, A3, Th66; :: thesis: verum
end;
assume A4: for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ; :: thesis: A c= the_rank_of X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the_rank_of X )
assume A5: x in A ; :: thesis: x in the_rank_of X
then reconsider x = x as Ordinal ;
consider Y being set such that
A6: Y in X and
A7: x c= the_rank_of Y by A4, A5;
the_rank_of Y in the_rank_of X by A6, Th68;
hence x in the_rank_of X by A7, ORDINAL1:12; :: thesis: verum