Theorem elrnsiga

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

	Ref	Expression
Assertion	elrnsiga	$$⊢S\in \mathrm{sigAlgebra}\left(O\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$

Proof

Step	Hyp	Ref	Expression
1		fvssunirn	$$⊢\mathrm{sigAlgebra}\left(O\right)\subseteq \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
2	1	sseli	$$⊢S\in \mathrm{sigAlgebra}\left(O\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$