Theorem sgon

Description: A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup S=\bigcup S$$
2		issgon	$$⊢S\in \mathrm{sigAlgebra}\left(\bigcup S\right)\leftrightarrow \left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup S=\bigcup S\right)$$
3	2	biimpri	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup S=\bigcup S\right)\to S\in \mathrm{sigAlgebra}\left(\bigcup S\right)$$
4	1 3	mpan2	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to S\in \mathrm{sigAlgebra}\left(\bigcup S\right)$$