Theorem salgenuni

Description: The base set of the sigma-algebra generated by a set is the union of the set itself. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salgenuni.x	$$⊢\phi \to X\in V$$
	salgenuni.s	$$⊢S=\mathrm{SalGen}\left(X\right)$$
	salgenuni.u	$$⊢U=\bigcup X$$
Assertion	salgenuni	$$⊢\phi \to \bigcup S=U$$

Proof

Step	Hyp	Ref	Expression
1		salgenuni.x	$$⊢\phi \to X\in V$$
2		salgenuni.s	$$⊢S=\mathrm{SalGen}\left(X\right)$$
3		salgenuni.u	$$⊢U=\bigcup X$$
4	2	a1i	$$⊢\phi \to S=\mathrm{SalGen}\left(X\right)$$
5		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\}$$
6	1 5	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\}$$
7	4 6	eqtrd	$$⊢\phi \to S=\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
8	7	unieqd	$$⊢\phi \to \bigcup S=\bigcup \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
9		ssrab2	$$⊢\left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\subseteq \mathrm{SAlg}$$
10	9	a1i	$$⊢\phi \to \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\subseteq \mathrm{SAlg}$$
11		salgenn0	$$⊢X\in V\to \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\ne \varnothing$$
12	1 11	syl	$$⊢\phi \to \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\ne \varnothing$$
13		unieq	$$⊢s=t\to \bigcup s=\bigcup t$$
14	13	eqeq1d	$$⊢s=t\to \left(\bigcup s=\bigcup X\leftrightarrow \bigcup t=\bigcup X\right)$$
15		sseq2	$$⊢s=t\to \left(X\subseteq s\leftrightarrow X\subseteq t\right)$$
16	14 15	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)$$
17	16	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)$$
18	17	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)$$
19	18	simprld	$$⊢t\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to \bigcup t=\bigcup X$$
20	3	eqcomi	$$⊢\bigcup X=U$$
21	20	a1i	$$⊢t\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to \bigcup X=U$$
22	19 21	eqtrd	$$⊢t\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\to \bigcup t=U$$
23	22	adantl	$$⊢\left(\phi \wedge t\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\right)\to \bigcup t=U$$
24	10 12 23	intsaluni	$$⊢\phi \to \bigcup \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}=U$$
25	8 24	eqtrd	$$⊢\phi \to \bigcup S=U$$