Metamath Proof Explorer

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 R_{1} = R_{1} [On]$

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	$⊢ Lim dom R_{1}$
2		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
3		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
4		dfrn7	$⊢ dom R_{1} \subseteq On \to ran R_{1} = R_{1} [On]$
5	2 3 4	3syl	$⊢ Lim dom R_{1} \to ran R_{1} = R_{1} [On]$
6	1 5	ax-mp	$⊢ ran R_{1} = R_{1} [On]$