rankwflemb

Description: Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	rankwflemb	$⊢ 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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
17	16	simpli	$⊢ Fun R_{1}$
18		fvelima	$⊢ (Fun R_{1} \land y \in R_{1} [On]) \to \exists x \in On R_{1} (x) = y$
19	17 18	mpan	$⊢ y \in R_{1} [On] \to \exists x \in On R_{1} (x) = y$
20	15 19	impel	$⊢ (A \in y \land y \in R_{1} [On]) \to \exists x \in On A \in R_{1} (suc x)$
21	20	exlimiv	$⊢ \exists y (A \in y \land y \in R_{1} [On]) \to \exists x \in On A \in R_{1} (suc x)$
22	1 21	sylbi	$⊢ A \in ⋃ R_{1} [On] \to \exists x \in On A \in R_{1} (suc x)$
23		elfvdm	$⊢ A \in R_{1} (suc x) \to suc x \in dom R_{1}$
24		fvelrn	$⊢ (Fun R_{1} \land suc x \in dom R_{1}) \to R_{1} (suc x) \in ran R_{1}$
25	17 23 24	sylancr	$⊢ A \in R_{1} (suc x) \to R_{1} (suc x) \in ran R_{1}$
26		df-ima	$⊢ R_{1} [On] = ran ({R_{1} ↾}_{On})$
27		funrel	$⊢ Fun R_{1} \to Rel R_{1}$
28	17 27	ax-mp	$⊢ Rel R_{1}$
29	16	simpri	$⊢ Lim dom R_{1}$
30		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
31		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
32	29 30 31	mp2b	$⊢ dom R_{1} \subseteq On$
33		relssres	$⊢ (Rel R_{1} \land dom R_{1} \subseteq On) \to {R_{1} ↾}_{On} = R_{1}$
34	28 32 33	mp2an	$⊢ {R_{1} ↾}_{On} = R_{1}$
35	34	rneqi	$⊢ ran ({R_{1} ↾}_{On}) = ran R_{1}$
36	26 35	eqtri	$⊢ R_{1} [On] = ran R_{1}$
37	25 36	eleqtrrdi	$⊢ A \in R_{1} (suc x) \to R_{1} (suc x) \in R_{1} [On]$
38		elunii	$⊢ (A \in R_{1} (suc x) \land R_{1} (suc x) \in R_{1} [On]) \to A \in ⋃ R_{1} [On]$
39	37 38	mpdan	$⊢ A \in R_{1} (suc x) \to A \in ⋃ R_{1} [On]$
40	39	rexlimivw	$⊢ \exists x \in On A \in R_{1} (suc x) \to A \in ⋃ R_{1} [On]$
41	22 40	impbii	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists x \in On A \in R_{1} (suc x)$

Metamath Proof Explorer

Theorem rankwflemb

Proof