Theorem sigagenss

Description: The generated sigma-algebra is a subset of all sigma-algebras containing the generating set, i.e. the generated sigma-algebra is the smallest sigma-algebra containing the generating set, here A . (Contributed by Thierry Arnoux, 4-Jun-2017)

	Ref	Expression
Assertion	sigagenss	$$⊢\left(S\in \mathrm{sigAlgebra}\left(\bigcup A\right)\wedge A\subseteq S\right)\to 𝛔\left(A\right)\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		ssexg	$$⊢\left(A\subseteq S\wedge S\in \mathrm{sigAlgebra}\left(\bigcup A\right)\right)\to A\in \mathrm{V}$$
2	1	ancoms	$$⊢\left(S\in \mathrm{sigAlgebra}\left(\bigcup A\right)\wedge A\subseteq S\right)\to A\in \mathrm{V}$$
3		sigagenval	$$⊢A\in \mathrm{V}\to 𝛔\left(A\right)=\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}$$
4	2 3	syl	$$⊢\left(S\in \mathrm{sigAlgebra}\left(\bigcup A\right)\wedge A\subseteq S\right)\to 𝛔\left(A\right)=\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}$$
5		sseq2	$$⊢s=S\to \left(A\subseteq s\leftrightarrow A\subseteq S\right)$$
6	5	intminss	$$⊢\left(S\in \mathrm{sigAlgebra}\left(\bigcup A\right)\wedge A\subseteq S\right)\to \bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}\subseteq S$$
7	4 6	eqsstrd	$$⊢\left(S\in \mathrm{sigAlgebra}\left(\bigcup A\right)\wedge A\subseteq S\right)\to 𝛔\left(A\right)\subseteq S$$