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_{1}[ 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_{1}[C] ) holds

S_{1}[A]
_{1}[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

Rrank X in U

let U be Grothendieck; :: thesis: ( X in U implies Rrank X in U )

defpred S

Rrank A in U;

A1: for A being Ordinal st ( for C being Ordinal st C in A holds

S

S

proof

A14:
for O being Ordinal holds S
let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds

S_{1}[C] ) implies S_{1}[A] )

assume A2: for C being Ordinal st C in A holds

S_{1}[C]
; :: thesis: S_{1}[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_{1}( 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_{1}(x) ) )
from FUNCT_1:sch 3();

A5: rng v c= U

hence Rrank S in U by A5, A4, A3, Def3; :: thesis: verum

end;S

assume A2: for C being Ordinal st C in A holds

S

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

consider v being Function such that

A4: ( dom v = S & ( for x being object st x in S holds

v . x = H

A5: rng v c= U

proof

A10:
union (rng v) c= Rrank S
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;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

proof

Rrank S c= union (rng v)
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;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

proof

then
union (rng v) = Rrank S
by A10;
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;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

hence Rrank S in U by A5, A4, A3, Def3; :: thesis: verum

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