Theorem unielsiga

Description: A sigma-algebra contains its universe set. (Contributed by Thierry Arnoux, 13-Feb-2017) (Shortened by Thierry Arnoux, 6-Jun-2017.)

	Ref	Expression
Assertion	unielsiga	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup S\in S$$

Proof

Step	Hyp	Ref	Expression
1		sgon	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to S\in \mathrm{sigAlgebra}\left(\bigcup S\right)$$
2		baselsiga	$$⊢S\in \mathrm{sigAlgebra}\left(\bigcup S\right)\to \bigcup S\in S$$
3	1 2	syl	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup S\in S$$