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	⊢ ( 𝐴 ∈ dom 𝑅1 ↔ ( rank ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rankonidlem	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = 𝐴 ) )
2	1	simprd	⊢ ( 𝐴 ∈ dom 𝑅1 → ( rank ‘ 𝐴 ) = 𝐴 )
3		id	⊢ ( ( rank ‘ 𝐴 ) = 𝐴 → ( rank ‘ 𝐴 ) = 𝐴 )
4		rankdmr1	⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
5	3 4	eqeltrrdi	⊢ ( ( rank ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ dom 𝑅1 )
6	2 5	impbii	⊢ ( 𝐴 ∈ dom 𝑅1 ↔ ( rank ‘ 𝐴 ) = 𝐴 )