Metamath Proof Explorer

Theorem rankr1b

Description: A relationship between rank and R1 . See rankr1a for the membership version. (Contributed by NM, 15-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Hypothesis	rankr1b.1	$⊢ A \in V$
	Assertion	rankr1b	$⊢ B \in On \to (A \subseteq R_{1} (B) \leftrightarrow rank (A) \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	$⊢ A \in V$
2		r1fnon	$⊢ R_{1} Fn On$
3	2	fndmi	$⊢ dom R_{1} = On$
4	3	eleq2i	$⊢ B \in dom R_{1} \leftrightarrow B \in On$
5		unir1	$⊢ ⋃ R_{1} [On] = V$
6	1 5	eleqtrri	$⊢ A \in ⋃ R_{1} [On]$
7		rankr1bg	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \subseteq R_{1} (B) \leftrightarrow rank (A) \subseteq B)$
8	6 7	mpan	$⊢ B \in dom R_{1} \to (A \subseteq R_{1} (B) \leftrightarrow rank (A) \subseteq B)$
9	4 8	sylbir	$⊢ B \in On \to (A \subseteq R_{1} (B) \leftrightarrow rank (A) \subseteq B)$