Theorem elrnsiga

Description: Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017)

	Ref	Expression
Assertion	elrnsiga	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑆 ∈ ∪ ran sigAlgebra )

Proof

Step	Hyp	Ref	Expression
1		fvssunirn	⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ ∪ ran sigAlgebra
2	1	sseli	⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑆 ∈ ∪ ran sigAlgebra )