Theorem r1omfv

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

	Ref	Expression
Assertion	r1omfv	⊢ ( 𝑅1 ‘ ω ) = ∪ ( 𝑅1 “ ω )

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		limom	⊢ Lim ω
3		r1lim	⊢ ( ( ω ∈ V ∧ Lim ω ) → ( 𝑅1 ‘ ω ) = ∪ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) )
4	1 2 3	mp2an	⊢ ( 𝑅1 ‘ ω ) = ∪ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 )
5		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
6	5	simpli	⊢ Fun 𝑅1
7		funiunfv	⊢ ( Fun 𝑅1 → ∪ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ ω ) )
8	6 7	ax-mp	⊢ ∪ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ ω )
9	4 8	eqtri	⊢ ( 𝑅1 ‘ ω ) = ∪ ( 𝑅1 “ ω )