Metamath Proof Explorer

Theorem rankonid

Description: The rank of an ordinal number is itself. Proposition 9.18 of TakeutiZaring p. 79 and its converse. (Contributed by NM, 14-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankonid A dom R1 rank A = A


Step Hyp Ref Expression
1 rankonidlem A dom R1 A R1 On rank A = A
2 1 simprd A dom R1 rank A = A
3 id rank A = A rank A = A
4 rankdmr1 rank A dom R1
5 3 4 eqeltrrdi rank A = A A dom R1
6 2 5 impbii A dom R1 rank A = A