Theorem r1omfv

Description: Value of the cumulative hierarchy of sets function at _om . (Contributed by BTernaryTau, 25-Jan-2026)

	Ref	Expression
Assertion	r1omfv	|- ( R1 ` _om ) = U. ( R1 " _om )

Proof

Step	Hyp	Ref	Expression
1		omex	|- _om e. _V
2		limom	|- Lim _om
3		r1lim	|- ( ( _om e. _V /\ Lim _om ) -> ( R1 ` _om ) = U_ x e. _om ( R1 ` x ) )
4	1 2 3	mp2an	|- ( R1 ` _om ) = U_ x e. _om ( R1 ` x )
5		r1funlim	|- ( Fun R1 /\ Lim dom R1 )
6	5	simpli	|- Fun R1
7		funiunfv	|- ( Fun R1 -> U_ x e. _om ( R1 ` x ) = U. ( R1 " _om ) )
8	6 7	ax-mp	|- U_ x e. _om ( R1 ` x ) = U. ( R1 " _om )
9	4 8	eqtri	|- ( R1 ` _om ) = U. ( R1 " _om )