rankr1bg

Description: A relationship between rank and R1 . See rankr1ag for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	rankr1bg	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \subseteq R_{1} (B) \leftrightarrow rank (A) \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
2	1	simpri	$⊢ Lim dom R_{1}$
3		limsuc	$⊢ Lim dom R_{1} \to (B \in dom R_{1} \leftrightarrow suc B \in dom R_{1})$
4	2 3	ax-mp	$⊢ B \in dom R_{1} \leftrightarrow suc B \in dom R_{1}$
5		rankr1ag	$⊢ (A \in ⋃ R_{1} [On] \land suc B \in dom R_{1}) \to (A \in R_{1} (suc B) \leftrightarrow rank (A) \in suc B)$
6	4 5	sylan2b	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (suc B) \leftrightarrow rank (A) \in suc B)$
7		r1sucg	$⊢ B \in dom R_{1} \to R_{1} (suc B) = 𝒫 R_{1} (B)$
8	7	adantl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to R_{1} (suc B) = 𝒫 R_{1} (B)$
9	8	eleq2d	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (suc B) \leftrightarrow A \in 𝒫 R_{1} (B))$
10		fvex	$⊢ R_{1} (B) \in V$
11	10	elpw2	$⊢ A \in 𝒫 R_{1} (B) \leftrightarrow A \subseteq R_{1} (B)$
12	9 11	bitr2di	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \subseteq R_{1} (B) \leftrightarrow A \in R_{1} (suc B))$
13		rankon	$⊢ rank (A) \in On$
14		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
15	2 14	ax-mp	$⊢ Ord dom R_{1}$
16		ordelon	$⊢ (Ord dom R_{1} \land B \in dom R_{1}) \to B \in On$
17	15 16	mpan	$⊢ B \in dom R_{1} \to B \in On$
18	17	adantl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to B \in On$
19		onsssuc	$⊢ (rank (A) \in On \land B \in On) \to (rank (A) \subseteq B \leftrightarrow rank (A) \in suc B)$
20	13 18 19	sylancr	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (rank (A) \subseteq B \leftrightarrow rank (A) \in suc B)$
21	6 12 20	3bitr4d	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \subseteq R_{1} (B) \leftrightarrow rank (A) \subseteq B)$

Metamath Proof Explorer

Theorem rankr1bg

Proof