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 S1[ 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
S1[C] ) holds
S1[A]
proof
let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S1[C] ) implies S1[A] )

assume A2: for C being Ordinal st C in A holds
S1[C] ; :: thesis: S1[A]
assume A3: A in U ; :: thesis: Rank A in U
deffunc H1( 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 = H1(O) ) ) from A5: rng br c= U
proof
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;
A7: union (rng br) c= Rank A
proof
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 ;
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;
Rank A c= union (rng br)
proof
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 ;
A12: br . B in rng br by ;
br . B = bool (Rank B) by ;
hence x in union (rng br) by ; :: thesis: verum
end;
then Rank A = union (rng br) by A7;
hence Rank A in U by A5, Def3, A4, A3; :: thesis: verum
end;
for O being Ordinal holds S1[O] from hence ( A in U implies Rank A in U ) ; :: thesis: verum