Theorem salgenss

Description: The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set. Proposition 111G (b) of Fremlin1 p. 13. Notice that the condition "on the same base set" is needed, see the counterexample salgensscntex , where a sigma-algebra is shown that includes a set, but does not include the sigma-algebra generated (the key is that its base set is larger than the base set of the generating set). (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salgenss.x	$$⊢\phi \to X\in V$$
	salgenss.g	$$⊢G=\mathrm{SalGen}\left(X\right)$$
	salgenss.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	salgenss.i	$$⊢\phi \to X\subseteq S$$
	salgenss.u	$$⊢\phi \to \bigcup S=\bigcup X$$
Assertion	salgenss	$$⊢\phi \to G\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		salgenss.x	$$⊢\phi \to X\in V$$
2		salgenss.g	$$⊢G=\mathrm{SalGen}\left(X\right)$$
3		salgenss.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		salgenss.i	$$⊢\phi \to X\subseteq S$$
5		salgenss.u	$$⊢\phi \to \bigcup S=\bigcup X$$
6	2	a1i	$$⊢\phi \to G=\mathrm{SalGen}\left(X\right)$$
7		salgenval	$$⊢X\in V\to \mathrm{SalGen}\left(X\right)=\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
8	1 7	syl	$$⊢\phi \to \mathrm{SalGen}\left(X\right)=\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
9	6 8	eqtrd	$$⊢\phi \to G=\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
10	5 4	jca	$$⊢\phi \to \left(\bigcup S=\bigcup X\wedge X\subseteq S\right)$$
11	3 10	jca	$$⊢\phi \to \left(S\in \mathrm{SAlg}\wedge \left(\bigcup S=\bigcup X\wedge X\subseteq S\right)\right)$$
12		unieq	$$⊢s=S\to \bigcup s=\bigcup S$$
13	12	eqeq1d	$$⊢s=S\to \left(\bigcup s=\bigcup X\leftrightarrow \bigcup S=\bigcup X\right)$$
14		sseq2	$$⊢s=S\to \left(X\subseteq s\leftrightarrow X\subseteq S\right)$$
15	13 14	anbi12d	$$⊢s=S\to \left(\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\leftrightarrow \left(\bigcup S=\bigcup X\wedge X\subseteq S\right)\right)$$
16	15	elrab	$$⊢S\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\leftrightarrow \left(S\in \mathrm{SAlg}\wedge \left(\bigcup S=\bigcup X\wedge X\subseteq S\right)\right)$$
17	11 16	sylibr	$$⊢\phi \to S\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
18		intss1	$$⊢S\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\subseteq S$$
19	17 18	syl	$$⊢\phi \to \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\subseteq S$$
20	9 19	eqsstrd	$$⊢\phi \to G\subseteq S$$