Theorem r1wf

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

	Ref	Expression
Assertion	r1wf	⊢ ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V
2	1	pwid	⊢ ( 𝑅1 ‘ 𝐴 ) ∈ 𝒫 ( 𝑅1 ‘ 𝐴 )
3		r1suc	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
4	2 3	eleqtrrid	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) )
5		r1elwf	⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )
6	4 5	syl	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )
7		onwf	⊢ On ⊆ ∪ ( 𝑅1 “ On )
8		r1fnon	⊢ 𝑅1 Fn On
9	8	fndmi	⊢ dom 𝑅1 = On
10	9	eleq2i	⊢ ( 𝐴 ∈ dom 𝑅1 ↔ 𝐴 ∈ On )
11		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) = ∅ )
12	10 11	sylnbir	⊢ ( ¬ 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) = ∅ )
13		0elon	⊢ ∅ ∈ On
14	12 13	eqeltrdi	⊢ ( ¬ 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) ∈ On )
15	7 14	sselid	⊢ ( ¬ 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )
16	6 15	pm2.61i	⊢ ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On )