let O be Ordinal; :: thesis: ( O = the_rank_of X iff ( X c= Rank O & ( for B being Ordinal st X c= Rank B holds
O c= B ) ) )
thus ( O = the_rank_of X implies ( X c= Rank O & ( for B being Ordinal st X c= Rank B holds
O c= B ) ) ) :: thesis: ( X c= Rank O & ( for B being Ordinal st X c= Rank B holds
O c= B ) implies O = the_rank_of X )
proof
assume A1: O = the_rank_of X ; :: thesis: ( X c= Rank O & ( for B being Ordinal st X c= Rank B holds
O c= B ) )
then X in Rank (succ O) by Def8;
then X in bool (Rank O) by Lm2;
hence X c= Rank O ; :: thesis: for B being Ordinal st X c= Rank B holds
O c= B
let B be Ordinal; :: thesis: ( X c= Rank B implies O c= B )
assume X c= Rank B ; :: thesis: O c= B
then X in bool (Rank B) ;
then X in Rank (succ B) by Lm2;
hence O c= B by A1, Def8; :: thesis: verum
end;
assume X c= Rank O ; :: thesis: ( ex B being Ordinal st
( X c= Rank B & not O c= B ) or O = the_rank_of X )
then X in bool (Rank O) ;
then A2: X in Rank (succ O) by Lm2;
assume A3: for B being Ordinal st X c= Rank B holds
O c= B ; :: thesis: O = the_rank_of X
for B being Ordinal st X in Rank (succ B) holds
O c= B
proof
let B be Ordinal; :: thesis: ( X in Rank (succ B) implies O c= B )
assume X in Rank (succ B) ; :: thesis: O c= B
then X in bool (Rank B) by Lm2;
hence O c= B by A3; :: thesis: verum
end;
hence O = the_rank_of X by A2, Def8; :: thesis: verum