r1wf

Description: Each stage in the cumulative hierarchy is well-founded. (Contributed by BTernaryTau, 19-Jan-2026)

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

Step	Hyp	Ref	Expression
1		fvex	$⊢ R_{1} (A) \in V$
2	1	pwid	$⊢ R_{1} (A) \in 𝒫 R_{1} (A)$
3		r1suc	$⊢ A \in On \to R_{1} (suc A) = 𝒫 R_{1} (A)$
4	2 3	eleqtrrid	$⊢ A \in On \to R_{1} (A) \in R_{1} (suc A)$
5		r1elwf	$⊢ R_{1} (A) \in R_{1} (suc A) \to R_{1} (A) \in ⋃ R_{1} [On]$
6	4 5	syl	$⊢ A \in On \to R_{1} (A) \in ⋃ R_{1} [On]$
7		onwf	$⊢ On \subseteq ⋃ R_{1} [On]$
8		r1fnon	$⊢ R_{1} Fn On$
9	8	fndmi	$⊢ dom R_{1} = On$
10	9	eleq2i	$⊢ A \in dom R_{1} \leftrightarrow A \in On$
11		ndmfv	$⊢ \neg A \in dom R_{1} \to R_{1} (A) = \emptyset$
12	10 11	sylnbir	$⊢ \neg A \in On \to R_{1} (A) = \emptyset$
13		0elon	$⊢ \emptyset \in On$
14	12 13	eqeltrdi	$⊢ \neg A \in On \to R_{1} (A) \in On$
15	7 14	sselid	$⊢ \neg A \in On \to R_{1} (A) \in ⋃ R_{1} [On]$
16	6 15	pm2.61i	$⊢ R_{1} (A) \in ⋃ R_{1} [On]$

Metamath Proof Explorer