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₁[ 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₁[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]
assume A3: A in U ; :: thesis: Rank A in U
deffunc H₁( 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₁(O) ) ) from ORDINAL2:sch 2();
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 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;

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 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;

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 S₁[O] from ORDINAL1:sch 2(A1);
hence ( A in U implies Rank A in U ) ; :: thesis: verum