r1elwf

Description: Any member of the cumulative hierarchy is well-founded. (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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
2	1	simpri	$⊢ Lim dom R_{1}$
3		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
4		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
5	2 3 4	mp2b	$⊢ dom R_{1} \subseteq On$
6		elfvdm	$⊢ A \in R_{1} (B) \to B \in dom R_{1}$
7	5 6	sseldi	$⊢ A \in R_{1} (B) \to B \in On$
8		r1tr	$⊢ Tr R_{1} (B)$
9		trss	$⊢ Tr R_{1} (B) \to (A \in R_{1} (B) \to A \subseteq R_{1} (B))$
10	8 9	ax-mp	$⊢ A \in R_{1} (B) \to A \subseteq R_{1} (B)$
11		elpwg	$⊢ A \in R_{1} (B) \to (A \in 𝒫 R_{1} (B) \leftrightarrow A \subseteq R_{1} (B))$
12	10 11	mpbird	$⊢ A \in R_{1} (B) \to A \in 𝒫 R_{1} (B)$
13		r1sucg	$⊢ B \in dom R_{1} \to R_{1} (suc B) = 𝒫 R_{1} (B)$
14	6 13	syl	$⊢ A \in R_{1} (B) \to R_{1} (suc B) = 𝒫 R_{1} (B)$
15	12 14	eleqtrrd	$⊢ A \in R_{1} (B) \to A \in R_{1} (suc B)$
16		suceq	$⊢ x = B \to suc x = suc B$
17	16	fveq2d	$⊢ x = B \to R_{1} (suc x) = R_{1} (suc B)$
18	17	eleq2d	$⊢ x = B \to (A \in R_{1} (suc x) \leftrightarrow A \in R_{1} (suc B))$
19	18	rspcev	$⊢ (B \in On \land A \in R_{1} (suc B)) \to \exists x \in On A \in R_{1} (suc x)$
20	7 15 19	syl2anc	$⊢ A \in R_{1} (B) \to \exists x \in On A \in R_{1} (suc x)$
21		rankwflemb	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists x \in On A \in R_{1} (suc x)$
22	20 21	sylibr	$⊢ A \in R_{1} (B) \to A \in ⋃ R_{1} [On]$

Metamath Proof Explorer

Theorem r1elwf

Proof