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\in \mathrm{dom}{R}_1\leftrightarrow \mathrm{rank}\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		rankonidlem	$$⊢A\in \mathrm{dom}{R}_1\to \left(A\in \bigcup R_1\left[\mathrm{On}\right]\wedge \mathrm{rank}\left(A\right)=A\right)$$
2	1	simprd	$$⊢A\in \mathrm{dom}{R}_1\to \mathrm{rank}\left(A\right)=A$$
3		id	$$⊢\mathrm{rank}\left(A\right)=A\to \mathrm{rank}\left(A\right)=A$$
4		rankdmr1	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{dom}{R}_1$$
5	3 4	eqeltrrdi	$$⊢\mathrm{rank}\left(A\right)=A\to A\in \mathrm{dom}{R}_1$$
6	2 5	impbii	$$⊢A\in \mathrm{dom}{R}_1\leftrightarrow \mathrm{rank}\left(A\right)=A$$