r1elwf

Description: Any element of (any stage of) the cumulative hierarchy of sets is well-founded (recall that U. ( R1 " On ) is the class of well-founded sets). (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	r1elwf	$⊢ A \in R_{1} (B) \to A \in ⋃ R_{1} [On]$

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	$⊢ Lim dom R_{1}$
2		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
3		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
4	1 2 3	mp2b	$⊢ dom R_{1} \subseteq On$
5		elfvdm	$⊢ A \in R_{1} (B) \to B \in dom R_{1}$
6	4 5	sselid	$⊢ A \in R_{1} (B) \to B \in On$
7		r1tr	$⊢ Tr R_{1} (B)$
8		trss	$⊢ Tr R_{1} (B) \to (A \in R_{1} (B) \to A \subseteq R_{1} (B))$
9	7 8	ax-mp	$⊢ A \in R_{1} (B) \to A \subseteq R_{1} (B)$
10		elpwg	$⊢ A \in R_{1} (B) \to (A \in 𝒫 R_{1} (B) \leftrightarrow A \subseteq R_{1} (B))$
11	9 10	mpbird	$⊢ A \in R_{1} (B) \to A \in 𝒫 R_{1} (B)$
12		r1sucg	$⊢ B \in dom R_{1} \to R_{1} (suc B) = 𝒫 R_{1} (B)$
13	5 12	syl	$⊢ A \in R_{1} (B) \to R_{1} (suc B) = 𝒫 R_{1} (B)$
14	11 13	eleqtrrd	$⊢ A \in R_{1} (B) \to A \in R_{1} (suc B)$
15		suceq	$⊢ x = B \to suc x = suc B$
16	15	fveq2d	$⊢ x = B \to R_{1} (suc x) = R_{1} (suc B)$
17	16	eleq2d	$⊢ x = B \to (A \in R_{1} (suc x) \leftrightarrow A \in R_{1} (suc B))$
18	17	rspcev	$⊢ (B \in On \land A \in R_{1} (suc B)) \to \exists x \in On A \in R_{1} (suc x)$
19	6 14 18	syl2anc	$⊢ A \in R_{1} (B) \to \exists x \in On A \in R_{1} (suc x)$
20		rankwflemb	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists x \in On A \in R_{1} (suc x)$
21	19 20	sylibr	$⊢ A \in R_{1} (B) \to A \in ⋃ R_{1} [On]$

Metamath Proof Explorer

Theorem r1elwf

Proof