Theorem rnr1

Description: The range of the cumulative hierarchy of sets function. This is the class of all stages of the cumulative hierarchy of sets, not the class of all sets in some stage of the cumulative hierarchy (that is U. ran R1 ).

This statement does not require the axiom of replacement by avoiding using r1fnon . (Contributed by BJ, 27-Sep-2026)

	Ref	Expression
Assertion	rnr1	⊢ ran 𝑅1 = ( 𝑅1 “ On )

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	⊢ Lim dom 𝑅1
2		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
3		ordsson	⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
4		dfrn7	⊢ ( dom 𝑅1 ⊆ On → ran 𝑅1 = ( 𝑅1 “ On ) )
5	2 3 4	3syl	⊢ ( Lim dom 𝑅1 → ran 𝑅1 = ( 𝑅1 “ On ) )
6	1 5	ax-mp	⊢ ran 𝑅1 = ( 𝑅1 “ On )