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 e. dom R1 <-> ( rank ` A ) = A )

Proof

Step	Hyp	Ref	Expression
1		rankonidlem	|- ( A e. dom R1 -> ( A e. U. ( R1 " On ) /\ ( rank ` A ) = A ) )
2	1	simprd	|- ( A e. dom R1 -> ( rank ` A ) = A )
3		id	|- ( ( rank ` A ) = A -> ( rank ` A ) = A )
4		rankdmr1	|- ( rank ` A ) e. dom R1
5	3 4	eqeltrrdi	|- ( ( rank ` A ) = A -> A e. dom R1 )
6	2 5	impbii	|- ( A e. dom R1 <-> ( rank ` A ) = A )