Theorem issalgend

Description: One side of dfsalgen2 . If a sigma-algebra on U. X includes X and it is included in all the sigma-algebras with such two properties, then it is the sigma-algebra generated by X . (Contributed by Glauco Siliprandi, 3-Jan-2021)

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

Proof

Step	Hyp	Ref	Expression
1		issalgend.x	$$⊢\phi \to X\in V$$
2		issalgend.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
3		issalgend.u	$$⊢\phi \to \bigcup S=\bigcup X$$
4		issalgend.i	$$⊢\phi \to X\subseteq S$$
5		issalgend.a	$$⊢\left(\phi \wedge \left(y\in \mathrm{SAlg}\wedge \bigcup y=\bigcup X\wedge X\subseteq y\right)\right)\to S\subseteq y$$
6		eqid	$$⊢\mathrm{SalGen}\left(X\right)=\mathrm{SalGen}\left(X\right)$$
7	1 6 2 4 3	salgenss	$$⊢\phi \to \mathrm{SalGen}\left(X\right)\subseteq S$$
8		simpl	$$⊢\left(\phi \wedge y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\right)\to \phi$$
9		elrabi	$$⊢y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to y\in \mathrm{SAlg}$$
10	9	adantl	$$⊢\left(\phi \wedge y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\right)\to y\in \mathrm{SAlg}$$
11		unieq	$$⊢s=y\to \bigcup s=\bigcup y$$
12	11	eqeq1d	$$⊢s=y\to \left(\bigcup s=\bigcup X\leftrightarrow \bigcup y=\bigcup X\right)$$
13		sseq2	$$⊢s=y\to \left(X\subseteq s\leftrightarrow X\subseteq y\right)$$
14	12 13	anbi12d	$$⊢s=y\to \left(\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\leftrightarrow \left(\bigcup y=\bigcup X\wedge X\subseteq y\right)\right)$$
15	14	elrab	$$⊢y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\leftrightarrow \left(y\in \mathrm{SAlg}\wedge \left(\bigcup y=\bigcup X\wedge X\subseteq y\right)\right)$$
16	15	biimpi	$$⊢y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to \left(y\in \mathrm{SAlg}\wedge \left(\bigcup y=\bigcup X\wedge X\subseteq y\right)\right)$$
17	16	simprld	$$⊢y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to \bigcup y=\bigcup X$$
18	17	adantl	$$⊢\left(\phi \wedge y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\right)\to \bigcup y=\bigcup X$$
19	16	simprrd	$$⊢y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to X\subseteq y$$
20	19	adantl	$$⊢\left(\phi \wedge y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\right)\to X\subseteq y$$
21	8 10 18 20 5	syl13anc	$$⊢\left(\phi \wedge y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\right)\to S\subseteq y$$
22	21	ralrimiva	$$⊢\phi \to \forall y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}S\subseteq y$$
23		ssint	$$⊢S\subseteq \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\leftrightarrow \forall y\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}S\subseteq y$$
24	22 23	sylibr	$$⊢\phi \to S\subseteq \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
25		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\}$$
26	1 25	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\}$$
27	24 26	sseqtrrd	$$⊢\phi \to S\subseteq \mathrm{SalGen}\left(X\right)$$
28	7 27	eqssd	$$⊢\phi \to \mathrm{SalGen}\left(X\right)=S$$