Theorem unir1regs

Description: The cumulative hierarchy of sets covers the universe. This version of unir1 replaces setind with setindregs . (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	unir1regs	⊢ ∪ ( 𝑅1 “ On ) = V

Proof

Step	Hyp	Ref	Expression
1		setindregs	⊢ ( ∀ 𝑥 ( 𝑥 ⊆ ∪ ( 𝑅1 “ On ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) → ∪ ( 𝑅1 “ On ) = V )
2		vex	⊢ 𝑥 ∈ V
3	2	r1elss	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
4	3	biimpri	⊢ ( 𝑥 ⊆ ∪ ( 𝑅1 “ On ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
5	1 4	mpg	⊢ ∪ ( 𝑅1 “ On ) = V