Theorem sssalgen

Description: A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypothesis	sssalgen.1	$$⊢S=\mathrm{SalGen}\left(X\right)$$
Assertion	sssalgen	$$⊢X\in V\to X\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		sssalgen.1	$$⊢S=\mathrm{SalGen}\left(X\right)$$
2		ssint	$$⊢X\subseteq \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\leftrightarrow \forall t\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}X\subseteq t$$
3		unieq	$$⊢s=t\to \bigcup s=\bigcup t$$
4	3	eqeq1d	$$⊢s=t\to \left(\bigcup s=\bigcup X\leftrightarrow \bigcup t=\bigcup X\right)$$
5		sseq2	$$⊢s=t\to \left(X\subseteq s\leftrightarrow X\subseteq t\right)$$
6	4 5	anbi12d	$$⊢s=t\to \left(\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\leftrightarrow \left(\bigcup t=\bigcup X\wedge X\subseteq t\right)\right)$$
7	6	elrab	$$⊢t\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\leftrightarrow \left(t\in \mathrm{SAlg}\wedge \left(\bigcup t=\bigcup X\wedge X\subseteq t\right)\right)$$
8	7	biimpi	$$⊢t\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to \left(t\in \mathrm{SAlg}\wedge \left(\bigcup t=\bigcup X\wedge X\subseteq t\right)\right)$$
9	8	simprrd	$$⊢t\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to X\subseteq t$$
10	2 9	mprgbir	$$⊢X\subseteq \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
11	10	a1i	$$⊢X\in V\to X\subseteq \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
12		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\}$$
13	1 12	eqtr2id	$$⊢X\in V\to \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}=S$$
14	11 13	sseqtrd	$$⊢X\in V\to X\subseteq S$$