Theorem r1dmlim

Description: The domain of the cumulative hierarchy of sets function is a limit ordinal. This weak form of r1fnon avoids ax-rep . (Contributed by Mario Carneiro, 16-Nov-2014) Extract this statement from its conjunction with r1fun . (Revised by BJ, 27-Sep-2026)

	Ref	Expression
Assertion	r1dmlim	⊢ Lim dom 𝑅1

Proof

Step	Hyp	Ref	Expression
1		rdgdmlim	⊢ Lim dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
2		df-r1	⊢ 𝑅1 = rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
3	2	dmeqi	⊢ dom 𝑅1 = dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
4		limeq	⊢ ( dom 𝑅1 = dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) → ( Lim dom 𝑅1 ↔ Lim dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ) )
5	3 4	ax-mp	⊢ ( Lim dom 𝑅1 ↔ Lim dom rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) )
6	1 5	mpbir	⊢ Lim dom 𝑅1