Theorem salgenval

Description: The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Assertion	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\}$$

Proof

Step	Hyp	Ref	Expression
1		df-salgen	$$⊢\mathrm{SalGen}=\left(x\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}\right)$$
2	1	a1i	$$⊢X\in V\to \mathrm{SalGen}=\left(x\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}\right)$$
3		unieq	$$⊢x=X\to \bigcup x=\bigcup X$$
4	3	eqeq2d	$$⊢x=X\to \left(\bigcup s=\bigcup x\leftrightarrow \bigcup s=\bigcup X\right)$$
5		sseq1	$$⊢x=X\to \left(x\subseteq s\leftrightarrow X\subseteq s\right)$$
6	4 5	anbi12d	$$⊢x=X\to \left(\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\leftrightarrow \left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right)$$
7	6	rabbidv	$$⊢x=X\to \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}=\left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
8	7	inteqd	$$⊢x=X\to \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}=\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
9	8	adantl	$$⊢\left(X\in V\wedge x=X\right)\to \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}=\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
10		elex	$$⊢X\in V\to X\in \mathrm{V}$$
11		uniexg	$$⊢X\in V\to \bigcup X\in \mathrm{V}$$
12		pwsal	$$⊢\bigcup X\in \mathrm{V}\to 𝒫\bigcup X\in \mathrm{SAlg}$$
13	11 12	syl	$$⊢X\in V\to 𝒫\bigcup X\in \mathrm{SAlg}$$
14		unipw	$$⊢\bigcup 𝒫\bigcup X=\bigcup X$$
15	14	a1i	$$⊢X\in V\to \bigcup 𝒫\bigcup X=\bigcup X$$
16		pwuni	$$⊢X\subseteq 𝒫\bigcup X$$
17	16	a1i	$$⊢X\in V\to X\subseteq 𝒫\bigcup X$$
18	13 15 17	jca32	$$⊢X\in V\to \left(𝒫\bigcup X\in \mathrm{SAlg}\wedge \left(\bigcup 𝒫\bigcup X=\bigcup X\wedge X\subseteq 𝒫\bigcup X\right)\right)$$
19		unieq	$$⊢s=𝒫\bigcup X\to \bigcup s=\bigcup 𝒫\bigcup X$$
20	19	eqeq1d	$$⊢s=𝒫\bigcup X\to \left(\bigcup s=\bigcup X\leftrightarrow \bigcup 𝒫\bigcup X=\bigcup X\right)$$
21		sseq2	$$⊢s=𝒫\bigcup X\to \left(X\subseteq s\leftrightarrow X\subseteq 𝒫\bigcup X\right)$$
22	20 21	anbi12d	$$⊢s=𝒫\bigcup X\to \left(\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\leftrightarrow \left(\bigcup 𝒫\bigcup X=\bigcup X\wedge X\subseteq 𝒫\bigcup X\right)\right)$$
23	22	elrab	$$⊢𝒫\bigcup X\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\leftrightarrow \left(𝒫\bigcup X\in \mathrm{SAlg}\wedge \left(\bigcup 𝒫\bigcup X=\bigcup X\wedge X\subseteq 𝒫\bigcup X\right)\right)$$
24	18 23	sylibr	$$⊢X\in V\to 𝒫\bigcup X\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
25	24	ne0d	$$⊢X\in V\to \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\ne \varnothing$$
26		intex	$$⊢\left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\ne \varnothing \leftrightarrow \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\in \mathrm{V}$$
27	25 26	sylib	$$⊢X\in V\to \bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\in \mathrm{V}$$
28	2 9 10 27	fvmptd	$$⊢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\}$$