rankr1ai

		Ref	Expression
	Assertion	rankr1ai	$⊢ A \in R_{1} (B) \to rank (A) \in B$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ A \in R_{1} (B) \to B \in dom R_{1}$
2		r1val1	$⊢ B \in dom R_{1} \to R_{1} (B) = ⋃_{x \in B} 𝒫 R_{1} (x)$
3	2	eleq2d	$⊢ B \in dom R_{1} \to (A \in R_{1} (B) \leftrightarrow A \in ⋃_{x \in B} 𝒫 R_{1} (x))$
4		eliun	$⊢ A \in ⋃_{x \in B} 𝒫 R_{1} (x) \leftrightarrow \exists x \in B A \in 𝒫 R_{1} (x)$
5	3 4	bitrdi	$⊢ B \in dom R_{1} \to (A \in R_{1} (B) \leftrightarrow \exists x \in B A \in 𝒫 R_{1} (x))$
6		r1dmlim	$⊢ Lim dom R_{1}$
7		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
8	6 7	ax-mp	$⊢ Ord dom R_{1}$
9		ordtr1	$⊢ Ord dom R_{1} \to ((x \in B \land B \in dom R_{1}) \to x \in dom R_{1})$
10	8 9	ax-mp	$⊢ (x \in B \land B \in dom R_{1}) \to x \in dom R_{1}$
11	10	ancoms	$⊢ (B \in dom R_{1} \land x \in B) \to x \in dom R_{1}$
12		r1sucg	$⊢ x \in dom R_{1} \to R_{1} (suc x) = 𝒫 R_{1} (x)$
13	12	eleq2d	$⊢ x \in dom R_{1} \to (A \in R_{1} (suc x) \leftrightarrow A \in 𝒫 R_{1} (x))$
14	11 13	syl	$⊢ (B \in dom R_{1} \land x \in B) \to (A \in R_{1} (suc x) \leftrightarrow A \in 𝒫 R_{1} (x))$
15		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
16	8 15	ax-mp	$⊢ dom R_{1} \subseteq On$
17	16 11	sselid	$⊢ (B \in dom R_{1} \land x \in B) \to x \in On$
18		rabid	$⊢ x \in \{x \in On \| A \in R_{1} (suc x)\} \leftrightarrow (x \in On \land A \in R_{1} (suc x))$
19		intss1	$⊢ x \in \{x \in On \| A \in R_{1} (suc x)\} \to ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x$
20	18 19	sylbir	$⊢ (x \in On \land A \in R_{1} (suc x)) \to ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x$
21	17 20	sylan	$⊢ ((B \in dom R_{1} \land x \in B) \land A \in R_{1} (suc x)) \to ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x$
22	21	ex	$⊢ (B \in dom R_{1} \land x \in B) \to (A \in R_{1} (suc x) \to ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x)$
23	14 22	sylbird	$⊢ (B \in dom R_{1} \land x \in B) \to (A \in 𝒫 R_{1} (x) \to ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x)$
24	23	reximdva	$⊢ B \in dom R_{1} \to (\exists x \in B A \in 𝒫 R_{1} (x) \to \exists x \in B ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x)$
25	5 24	sylbid	$⊢ B \in dom R_{1} \to (A \in R_{1} (B) \to \exists x \in B ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x)$
26	1 25	mpcom	$⊢ A \in R_{1} (B) \to \exists x \in B ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x$
27		r1elwf	$⊢ A \in R_{1} (B) \to A \in ⋃ R_{1} [On]$
28		rankvalb	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$
29	27 28	syl	$⊢ A \in R_{1} (B) \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$
30	29	sseq1d	$⊢ A \in R_{1} (B) \to (rank (A) \subseteq x \leftrightarrow ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x)$
31	30	adantr	$⊢ (A \in R_{1} (B) \land x \in B) \to (rank (A) \subseteq x \leftrightarrow ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x)$
32		rankon	$⊢ rank (A) \in On$
33	16 1	sselid	$⊢ A \in R_{1} (B) \to B \in On$
34		ontr2	$⊢ (rank (A) \in On \land B \in On) \to ((rank (A) \subseteq x \land x \in B) \to rank (A) \in B)$
35	32 33 34	sylancr	$⊢ A \in R_{1} (B) \to ((rank (A) \subseteq x \land x \in B) \to rank (A) \in B)$
36	35	expcomd	$⊢ A \in R_{1} (B) \to (x \in B \to (rank (A) \subseteq x \to rank (A) \in B))$
37	36	imp	$⊢ (A \in R_{1} (B) \land x \in B) \to (rank (A) \subseteq x \to rank (A) \in B)$
38	31 37	sylbird	$⊢ (A \in R_{1} (B) \land x \in B) \to (⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x \to rank (A) \in B)$
39	38	rexlimdva	$⊢ A \in R_{1} (B) \to (\exists x \in B ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x \to rank (A) \in B)$
40	26 39	mpd	$⊢ A \in R_{1} (B) \to rank (A) \in B$

Metamath Proof Explorer

Theorem rankr1ai

Proof