rankr1id

Description: The rank of the hierarchy of an ordinal number is itself. (Contributed by NM, 14-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	rankr1id	$⊢ A \in dom R_{1} \leftrightarrow rank (R_{1} (A)) = A$

Step	Hyp	Ref	Expression
1		ssid	$⊢ R_{1} (A) \subseteq R_{1} (A)$
2		fvex	$⊢ R_{1} (A) \in V$
3	2	pwid	$⊢ R_{1} (A) \in 𝒫 R_{1} (A)$
4		r1sucg	$⊢ A \in dom R_{1} \to R_{1} (suc A) = 𝒫 R_{1} (A)$
5	3 4	eleqtrrid	$⊢ A \in dom R_{1} \to R_{1} (A) \in R_{1} (suc A)$
6		r1elwf	$⊢ R_{1} (A) \in R_{1} (suc A) \to R_{1} (A) \in ⋃ R_{1} [On]$
7	5 6	syl	$⊢ A \in dom R_{1} \to R_{1} (A) \in ⋃ R_{1} [On]$
8		rankr1bg	$⊢ (R_{1} (A) \in ⋃ R_{1} [On] \land A \in dom R_{1}) \to (R_{1} (A) \subseteq R_{1} (A) \leftrightarrow rank (R_{1} (A)) \subseteq A)$
9	7 8	mpancom	$⊢ A \in dom R_{1} \to (R_{1} (A) \subseteq R_{1} (A) \leftrightarrow rank (R_{1} (A)) \subseteq A)$
10	1 9	mpbii	$⊢ A \in dom R_{1} \to rank (R_{1} (A)) \subseteq A$
11		rankonid	$⊢ A \in dom R_{1} \leftrightarrow rank (A) = A$
12	11	biimpi	$⊢ A \in dom R_{1} \to rank (A) = A$
13		onssr1	$⊢ A \in dom R_{1} \to A \subseteq R_{1} (A)$
14		rankssb	$⊢ R_{1} (A) \in ⋃ R_{1} [On] \to (A \subseteq R_{1} (A) \to rank (A) \subseteq rank (R_{1} (A)))$
15	7 13 14	sylc	$⊢ A \in dom R_{1} \to rank (A) \subseteq rank (R_{1} (A))$
16	12 15	eqsstrrd	$⊢ A \in dom R_{1} \to A \subseteq rank (R_{1} (A))$
17	10 16	eqssd	$⊢ A \in dom R_{1} \to rank (R_{1} (A)) = A$
18		id	$⊢ rank (R_{1} (A)) = A \to rank (R_{1} (A)) = A$
19		rankdmr1	$⊢ rank (R_{1} (A)) \in dom R_{1}$
20	18 19	eqeltrrdi	$⊢ rank (R_{1} (A)) = A \to A \in dom R_{1}$
21	17 20	impbii	$⊢ A \in dom R_{1} \leftrightarrow rank (R_{1} (A)) = A$

Metamath Proof Explorer