let X be set ; :: thesis: for U being Grothendieck st X in U holds
Rrank X in U
let U be Grothendieck; :: thesis: ( X in U implies Rrank X in U )
defpred S₁[ Ordinal] means for A being set st the_rank_of A in $1 & A in U holds
Rrank A in U;
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
S₁[C] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S₁[C] ) implies S₁[A] )
assume A2: for C being Ordinal st C in A holds
S₁[C] ; :: thesis: S₁[A]
let S be set ; :: thesis: ( the_rank_of S in A & S in U implies Rrank S in U )
assume A3: ( the_rank_of S in A & S in U ) ; :: thesis: Rrank S in U
deffunc H₁( object ) -> Element of K28(K28((Rrank $1))) = bool (Rrank $1);
consider v being Function such that
A4: ( dom v = S & ( for x being object st x in S holds
v . x = H₁(x) ) ) from FUNCT_1:sch 3();
A5: rng v c= U

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng v or y in U )
assume A6: y in rng v ; :: thesis: y in U
consider x being object such that
A7: ( x in dom v & v . x = y ) by A6, FUNCT_1:def 3;
succ (the_rank_of x) c= the_rank_of S by ORDINAL1:21, A7, A4, CLASSES1:68;
then A8: for S being set st the_rank_of S in succ (the_rank_of x) & S in U holds
Rrank S in U by A2, A3;
A9: x in U by A3, Th13, A7, A4;
Rrank x in U by A8, A9, ORDINAL1:6;
then bool (Rrank x) in U by Def1;
hence y in U by A7, A4; :: thesis: verum

end;

A10: union (rng v) c= Rrank S

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union (rng v) or a in Rrank S )
assume a in union (rng v) ; :: thesis: a in Rrank S
then consider b being set such that
A11: ( a in b & b in rng v ) by TARSKI:def 4;
consider x being object such that
A12: ( x in dom v & v . x = b ) by A11, FUNCT_1:def 3;
reconsider a = a, b = b, x = x as set by TARSKI:1;
b = bool (Rrank x) by A12, A4;
hence a in Rrank S by A11, A12, A4, Th4; :: thesis: verum

end;

Rrank S c= union (rng v)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Rrank S or x in union (rng v) )
assume x in Rrank S ; :: thesis: x in union (rng v)
then consider a being set such that
A13: ( a in S & x in bool (Rrank a) ) by Th4;
( v . a = bool (Rrank a) & v . a in rng v ) by A13, A4, FUNCT_1:def 3;
hence x in union (rng v) by A13, TARSKI:def 4; :: thesis: verum

end;

then union (rng v) = Rrank S by A10;
hence Rrank S in U by A5, A4, A3, Def3; :: thesis: verum

end;

A14: for O being Ordinal holds S₁[O] from ORDINAL1:sch 2(A1);
the_rank_of X in succ (the_rank_of X) by ORDINAL1:6;
hence ( X in U implies Rrank X in U ) by A14; :: thesis: verum