Metamath Proof Explorer

Theorem onrankid

Description: The rank of an ordinal number is itself. (Contributed by BTernaryTau, 3-Jul-2026)

Ref Expression
Assertion onrankid 
|- ( A e. On <-> ( rank ` A ) = A )

Proof

Step Hyp Ref Expression
1 r1fnon 
 |-  R1 Fn On
2 1 fndmi 
 |-  dom R1 = On
3 2 eleq2i 
 |-  ( A e. dom R1 <-> A e. On )
4 rankonid 
 |-  ( A e. dom R1 <-> ( rank ` A ) = A )
5 3 4 bitr3i 
 |-  ( A e. On <-> ( rank ` A ) = A )