let A be Ordinal; :: thesis: for U being Grothendieck st A in U holds

Rank A in U

let U be Grothendieck; :: thesis: ( A in U implies Rank A in U )

defpred S_{1}[ Ordinal] means ( $1 in U implies Rank $1 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);

hence ( A in U implies Rank A in U ) ; :: thesis: verum

Rank A in U

let U be Grothendieck; :: thesis: ( A in U implies Rank A in U )

defpred S

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

S

S

proof

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]

assume A3: A in U ; :: thesis: Rank A in U

deffunc H_{1}( Ordinal) -> Element of K28(K28((Rank $1))) = bool (Rank $1);

consider br being Sequence such that

A4: ( dom br = A & ( for O being Ordinal st O in A holds

br . O = H_{1}(O) ) )
from ORDINAL2:sch 2();

A5: rng br c= U

hence Rank A in U by A5, Def3, A4, A3; :: thesis: verum

end;S

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

S

assume A3: A in U ; :: thesis: Rank A in U

deffunc H

consider br being Sequence such that

A4: ( dom br = A & ( for O being Ordinal st O in A holds

br . O = H

A5: rng br c= U

proof

A7:
union (rng br) c= Rank A
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng br or y in U )

assume y in rng br ; :: thesis: y in U

then consider B being object such that

A6: ( B in dom br & br . B = y ) by FUNCT_1:def 3;

reconsider B = B as Ordinal by A6;

B in U by A6, A4, A3, Th13;

then ( bool (Rank B) in U & br . B = bool (Rank B) ) by A2, A4, A6, Def1;

hence y in U by A6; :: thesis: verum

end;assume y in rng br ; :: thesis: y in U

then consider B being object such that

A6: ( B in dom br & br . B = y ) by FUNCT_1:def 3;

reconsider B = B as Ordinal by A6;

B in U by A6, A4, A3, Th13;

then ( bool (Rank B) in U & br . B = bool (Rank B) ) by A2, A4, A6, Def1;

hence y in U by A6; :: thesis: verum

proof

Rank A c= union (rng br)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union (rng br) or z in Rank A )

assume z in union (rng br) ; :: thesis: z in Rank A

then consider y being set such that

A8: ( z in y & y in rng br ) by TARSKI:def 4;

consider B being object such that

A9: ( B in dom br & br . B = y ) by A8, FUNCT_1:def 3;

reconsider B = B as Ordinal by A9;

br . B = bool (Rank B) by A4, A9;

hence z in Rank A by A8, A9, A4, Th3; :: thesis: verum

end;assume z in union (rng br) ; :: thesis: z in Rank A

then consider y being set such that

A8: ( z in y & y in rng br ) by TARSKI:def 4;

consider B being object such that

A9: ( B in dom br & br . B = y ) by A8, FUNCT_1:def 3;

reconsider B = B as Ordinal by A9;

br . B = bool (Rank B) by A4, A9;

hence z in Rank A by A8, A9, A4, Th3; :: thesis: verum

proof

then
Rank A = union (rng br)
by A7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Rank A or x in union (rng br) )

assume A10: x in Rank A ; :: thesis: x in union (rng br)

reconsider X = x as set by TARSKI:1;

consider B being Ordinal such that

A11: ( B in A & X in bool (Rank B) ) by A10, Th3;

A12: br . B in rng br by A11, A4, FUNCT_1:def 3;

br . B = bool (Rank B) by A11, A4;

hence x in union (rng br) by A11, A12, TARSKI:def 4; :: thesis: verum

end;assume A10: x in Rank A ; :: thesis: x in union (rng br)

reconsider X = x as set by TARSKI:1;

consider B being Ordinal such that

A11: ( B in A & X in bool (Rank B) ) by A10, Th3;

A12: br . B in rng br by A11, A4, FUNCT_1:def 3;

br . B = bool (Rank B) by A11, A4;

hence x in union (rng br) by A11, A12, TARSKI:def 4; :: thesis: verum

hence Rank A in U by A5, Def3, A4, A3; :: thesis: verum

hence ( A in U implies Rank A in U ) ; :: thesis: verum