Theorem r1rankidb

Description: Any set is a subset of the hierarchy of its rank. (Contributed by Mario Carneiro, 3-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	r1rankidb	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to A\subseteq R_1\left(\mathrm{rank}\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)$$
2		rankdmr1	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{dom}{R}_1$$
3		rankr1bg	$$⊢\left(A\in \bigcup R_1\left[\mathrm{On}\right]\wedge \mathrm{rank}\left(A\right)\in \mathrm{dom}{R}_1\right)\to \left(A\subseteq R_1\left(\mathrm{rank}\left(A\right)\right)\leftrightarrow \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)\right)$$
4	2 3	mpan2	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \left(A\subseteq R_1\left(\mathrm{rank}\left(A\right)\right)\leftrightarrow \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)\right)$$
5	1 4	mpbiri	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to A\subseteq R_1\left(\mathrm{rank}\left(A\right)\right)$$