Theorem salgenn0

Description: The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Assertion	salgenn0	$$⊢X\in V\to \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		uniexg	$$⊢X\in V\to \bigcup X\in \mathrm{V}$$
2		pwsal	$$⊢\bigcup X\in \mathrm{V}\to 𝒫\bigcup X\in \mathrm{SAlg}$$
3	1 2	syl	$$⊢X\in V\to 𝒫\bigcup X\in \mathrm{SAlg}$$
4		unipw	$$⊢\bigcup 𝒫\bigcup X=\bigcup X$$
5	4	a1i	$$⊢X\in V\to \bigcup 𝒫\bigcup X=\bigcup X$$
6		pwuni	$$⊢X\subseteq 𝒫\bigcup X$$
7	6	a1i	$$⊢X\in V\to X\subseteq 𝒫\bigcup X$$
8	5 7	jca	$$⊢X\in V\to \left(\bigcup 𝒫\bigcup X=\bigcup X\wedge X\subseteq 𝒫\bigcup X\right)$$
9	3 8	jca	$$⊢X\in V\to \left(𝒫\bigcup X\in \mathrm{SAlg}\wedge \left(\bigcup 𝒫\bigcup X=\bigcup X\wedge X\subseteq 𝒫\bigcup X\right)\right)$$
10		unieq	$$⊢s=𝒫\bigcup X\to \bigcup s=\bigcup 𝒫\bigcup X$$
11	10	eqeq1d	$$⊢s=𝒫\bigcup X\to \left(\bigcup s=\bigcup X\leftrightarrow \bigcup 𝒫\bigcup X=\bigcup X\right)$$
12		sseq2	$$⊢s=𝒫\bigcup X\to \left(X\subseteq s\leftrightarrow X\subseteq 𝒫\bigcup X\right)$$
13	11 12	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)$$
14	13	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)$$
15	9 14	sylibr	$$⊢X\in V\to 𝒫\bigcup X\in \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}$$
16	15	ne0d	$$⊢X\in V\to \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup X\wedge X\subseteq s\right)\right\}\ne \varnothing$$