Theorem sigagenid

Description: The sigma-algebra generated by a sigma-algebra is itself. (Contributed by Thierry Arnoux, 4-Jun-2017)

	Ref	Expression
Assertion	sigagenid	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to 𝛔\left(S\right)=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		ssid	$$⊢S\subseteq S$$
3		sigagenss	$$⊢\left(S\in \mathrm{sigAlgebra}\left(\bigcup S\right)\wedge S\subseteq S\right)\to 𝛔\left(S\right)\subseteq S$$
4	1 2 3	sylancl	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to 𝛔\left(S\right)\subseteq S$$
5		sssigagen	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to S\subseteq 𝛔\left(S\right)$$
6	4 5	eqssd	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to 𝛔\left(S\right)=S$$