let X be set ; :: thesis: for A being Ordinal holds

( X in Rank A iff ex B being Ordinal st

( B in A & X in bool (Rank B) ) )

let A be Ordinal; :: thesis: ( X in Rank A iff ex B being Ordinal st

( B in A & X in bool (Rank B) ) )

thus ( X in Rank A implies ex B being Ordinal st

( B in A & X in bool (Rank B) ) ) :: thesis: ( ex B being Ordinal st

( B in A & X in bool (Rank B) ) implies X in Rank A )

( B in A & X in bool (Rank B) ) implies X in Rank A ) by CLASSES1:36, CLASSES1:41; :: thesis: verum

( X in Rank A iff ex B being Ordinal st

( B in A & X in bool (Rank B) ) )

let A be Ordinal; :: thesis: ( X in Rank A iff ex B being Ordinal st

( B in A & X in bool (Rank B) ) )

thus ( X in Rank A implies ex B being Ordinal st

( B in A & X in bool (Rank B) ) ) :: thesis: ( ex B being Ordinal st

( B in A & X in bool (Rank B) ) implies X in Rank A )

proof

thus
( ex B being Ordinal st
assume A1:
X in Rank A
; :: thesis: ex B being Ordinal st

( B in A & X in bool (Rank B) )

end;( B in A & X in bool (Rank B) )

per cases
( A is limit_ordinal or not A is limit_ordinal )
;

end;

suppose
A is limit_ordinal
; :: thesis: ex B being Ordinal st

( B in A & X in bool (Rank B) )

( B in A & X in bool (Rank B) )

then consider B being Ordinal such that

A3: ( B in A & X in Rank B ) by A1, CLASSES1:29, CLASSES1:31;

take B ; :: thesis: ( B in A & X in bool (Rank B) )

B c= B \/ {B} by XBOOLE_1:7;

then B c= succ B by ORDINAL1:def 1;

then Rank B c= Rank (succ B) by CLASSES1:37;

then X in Rank (succ B) by A3;

hence ( B in A & X in bool (Rank B) ) by A3, CLASSES1:30; :: thesis: verum

end;A3: ( B in A & X in Rank B ) by A1, CLASSES1:29, CLASSES1:31;

take B ; :: thesis: ( B in A & X in bool (Rank B) )

B c= B \/ {B} by XBOOLE_1:7;

then B c= succ B by ORDINAL1:def 1;

then Rank B c= Rank (succ B) by CLASSES1:37;

then X in Rank (succ B) by A3;

hence ( B in A & X in bool (Rank B) ) by A3, CLASSES1:30; :: thesis: verum

suppose
not A is limit_ordinal
; :: thesis: ex B being Ordinal st

( B in A & X in bool (Rank B) )

( B in A & X in bool (Rank B) )

then consider B being Ordinal such that

A4: A = succ B by ORDINAL1:29;

take B ; :: thesis: ( B in A & X in bool (Rank B) )

thus ( B in A & X in bool (Rank B) ) by A1, A4, ORDINAL1:6, CLASSES1:30; :: thesis: verum

end;A4: A = succ B by ORDINAL1:29;

take B ; :: thesis: ( B in A & X in bool (Rank B) )

thus ( B in A & X in bool (Rank B) ) by A1, A4, ORDINAL1:6, CLASSES1:30; :: thesis: verum

( B in A & X in bool (Rank B) ) implies X in Rank A ) by CLASSES1:36, CLASSES1:41; :: thesis: verum