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 R1 = ( R1 " On )

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	|- Lim dom R1
2		limord	|- ( Lim dom R1 -> Ord dom R1 )
3		ordsson	|- ( Ord dom R1 -> dom R1 C_ On )
4		dfrn7	|- ( dom R1 C_ On -> ran R1 = ( R1 " On ) )
5	2 3 4	3syl	|- ( Lim dom R1 -> ran R1 = ( R1 " On ) )
6	1 5	ax-mp	|- ran R1 = ( R1 " On )