r1omfv

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

		Ref	Expression
	Assertion	r1omfv	$⊢ R_{1} (ω) = ⋃ R_{1} [ω]$

Step	Hyp	Ref	Expression
1		omex	$⊢ ω \in V$
2		limom	$⊢ Lim ω$
3		r1lim	$⊢ (ω \in V \land Lim ω) \to R_{1} (ω) = ⋃_{x \in ω} R_{1} (x)$
4	1 2 3	mp2an	$⊢ R_{1} (ω) = ⋃_{x \in ω} R_{1} (x)$
5		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
6	5	simpli	$⊢ Fun R_{1}$
7		funiunfv	$⊢ Fun R_{1} \to ⋃_{x \in ω} R_{1} (x) = ⋃ R_{1} [ω]$
8	6 7	ax-mp	$⊢ ⋃_{x \in ω} R_{1} (x) = ⋃ R_{1} [ω]$
9	4 8	eqtri	$⊢ R_{1} (ω) = ⋃ R_{1} [ω]$

Metamath Proof Explorer