rankwflembOLD

Description: Obsolete version of rankwflemb as of 29-Sep-2026. (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	rankwflembOLD	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists x \in On A \in R_{1} (suc x)$

Proof

Step	Hyp	Ref	Expression
1		eluni	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists y (A \in y \land y \in R_{1} [On])$
2		eleq2	$⊢ R_{1} (x) = y \to (A \in R_{1} (x) \leftrightarrow A \in y)$
3	2	biimprcd	$⊢ A \in y \to (R_{1} (x) = y \to A \in R_{1} (x))$
4		r1tr	$⊢ Tr R_{1} (x)$
5		trss	$⊢ Tr R_{1} (x) \to (A \in R_{1} (x) \to A \subseteq R_{1} (x))$
6	4 5	ax-mp	$⊢ A \in R_{1} (x) \to A \subseteq R_{1} (x)$
7		elpwg	$⊢ A \in R_{1} (x) \to (A \in 𝒫 R_{1} (x) \leftrightarrow A \subseteq R_{1} (x))$
8	6 7	mpbird	$⊢ A \in R_{1} (x) \to A \in 𝒫 R_{1} (x)$
9		elfvdm	$⊢ A \in R_{1} (x) \to x \in dom R_{1}$
10		r1sucg	$⊢ x \in dom R_{1} \to R_{1} (suc x) = 𝒫 R_{1} (x)$
11	9 10	syl	$⊢ A \in R_{1} (x) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
12	8 11	eleqtrrd	$⊢ A \in R_{1} (x) \to A \in R_{1} (suc x)$
13	12	a1i	$⊢ x \in On \to (A \in R_{1} (x) \to A \in R_{1} (suc x))$
14	3 13	syl9	$⊢ A \in y \to (x \in On \to (R_{1} (x) = y \to A \in R_{1} (suc x)))$
15	14	reximdvai	$⊢ A \in y \to (\exists x \in On R_{1} (x) = y \to \exists x \in On A \in R_{1} (suc x))$
16		r1fun	$⊢ Fun R_{1}$
17		fvelima	$⊢ (Fun R_{1} \land y \in R_{1} [On]) \to \exists x \in On R_{1} (x) = y$
18	16 17	mpan	$⊢ y \in R_{1} [On] \to \exists x \in On R_{1} (x) = y$
19	15 18	impel	$⊢ (A \in y \land y \in R_{1} [On]) \to \exists x \in On A \in R_{1} (suc x)$
20	19	exlimiv	$⊢ \exists y (A \in y \land y \in R_{1} [On]) \to \exists x \in On A \in R_{1} (suc x)$
21	1 20	sylbi	$⊢ A \in ⋃ R_{1} [On] \to \exists x \in On A \in R_{1} (suc x)$
22		elfvdm	$⊢ A \in R_{1} (suc x) \to suc x \in dom R_{1}$
23		fvelrn	$⊢ (Fun R_{1} \land suc x \in dom R_{1}) \to R_{1} (suc x) \in ran R_{1}$
24	16 22 23	sylancr	$⊢ A \in R_{1} (suc x) \to R_{1} (suc x) \in ran R_{1}$
25		df-ima	$⊢ R_{1} [On] = ran ({R_{1} ↾}_{On})$
26		funrel	$⊢ Fun R_{1} \to Rel R_{1}$
27	16 26	ax-mp	$⊢ Rel R_{1}$
28		r1dmlim	$⊢ Lim dom R_{1}$
29		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
30		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
31	28 29 30	mp2b	$⊢ dom R_{1} \subseteq On$
32		relssres	$⊢ (Rel R_{1} \land dom R_{1} \subseteq On) \to {R_{1} ↾}_{On} = R_{1}$
33	27 31 32	mp2an	$⊢ {R_{1} ↾}_{On} = R_{1}$
34	33	rneqi	$⊢ ran ({R_{1} ↾}_{On}) = ran R_{1}$
35	25 34	eqtri	$⊢ R_{1} [On] = ran R_{1}$
36	24 35	eleqtrrdi	$⊢ A \in R_{1} (suc x) \to R_{1} (suc x) \in R_{1} [On]$
37		elunii	$⊢ (A \in R_{1} (suc x) \land R_{1} (suc x) \in R_{1} [On]) \to A \in ⋃ R_{1} [On]$
38	36 37	mpdan	$⊢ A \in R_{1} (suc x) \to A \in ⋃ R_{1} [On]$
39	38	rexlimivw	$⊢ \exists x \in On A \in R_{1} (suc x) \to A \in ⋃ R_{1} [On]$
40	21 39	impbii	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists x \in On A \in R_{1} (suc x)$

Metamath Proof Explorer

Theorem rankwflembOLD

Proof