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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
7	6	simpri	$⊢ Lim dom R_{1}$
8		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
9	7 8	ax-mp	$⊢ Ord dom R_{1}$
10		ordtr1	$⊢ Ord dom R_{1} \to ((x \in B \land B \in dom R_{1}) \to x \in dom R_{1})$
11	9 10	ax-mp	$⊢ (x \in B \land B \in dom R_{1}) \to x \in dom R_{1}$
12	11	ancoms	$⊢ (B \in dom R_{1} \land x \in B) \to x \in dom R_{1}$
13		r1sucg	$⊢ x \in dom R_{1} \to R_{1} (suc x) = 𝒫 R_{1} (x)$
14	13	eleq2d	$⊢ x \in dom R_{1} \to (A \in R_{1} (suc x) \leftrightarrow A \in 𝒫 R_{1} (x))$
15	12 14	syl	$⊢ (B \in dom R_{1} \land x \in B) \to (A \in R_{1} (suc x) \leftrightarrow A \in 𝒫 R_{1} (x))$
16		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
17	9 16	ax-mp	$⊢ dom R_{1} \subseteq On$
18	17 12	sselid	$⊢ (B \in dom R_{1} \land x \in B) \to x \in On$
19		rabid	$⊢ x \in \{x \in On \| A \in R_{1} (suc x)\} \leftrightarrow (x \in On \land A \in R_{1} (suc x))$
20		intss1	$⊢ x \in \{x \in On \| A \in R_{1} (suc x)\} \to ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x$
21	19 20	sylbir	$⊢ (x \in On \land A \in R_{1} (suc x)) \to ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x$
22	18 21	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$
23	22	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)$
24	15 23	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)$
25	24	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)$
26	5 25	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)$
27	1 26	mpcom	$⊢ A \in R_{1} (B) \to \exists x \in B ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x$
28		r1elwf	$⊢ A \in R_{1} (B) \to A \in ⋃ R_{1} [On]$
29		rankvalb	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$
30	28 29	syl	$⊢ A \in R_{1} (B) \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$
31	30	sseq1d	$⊢ A \in R_{1} (B) \to (rank (A) \subseteq x \leftrightarrow ⋂ \{x \in On \| A \in R_{1} (suc x)\} \subseteq x)$
32	31	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)$
33		rankon	$⊢ rank (A) \in On$
34	17 1	sselid	$⊢ A \in R_{1} (B) \to B \in On$
35		ontr2	$⊢ (rank (A) \in On \land B \in On) \to ((rank (A) \subseteq x \land x \in B) \to rank (A) \in B)$
36	33 34 35	sylancr	$⊢ A \in R_{1} (B) \to ((rank (A) \subseteq x \land x \in B) \to rank (A) \in B)$
37	36	expcomd	$⊢ A \in R_{1} (B) \to (x \in B \to (rank (A) \subseteq x \to rank (A) \in B))$
38	37	imp	$⊢ (A \in R_{1} (B) \land x \in B) \to (rank (A) \subseteq x \to rank (A) \in B)$
39	32 38	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)$
40	39	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)$
41	27 40	mpd	$⊢ A \in R_{1} (B) \to rank (A) \in B$

Metamath Proof Explorer

Theorem rankr1ai

Proof