Theorem pwsal

Description: The power set of a given set is a sigma-algebra (the so called discrete sigma-algebra). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pwsal	$$⊢X\in V\to 𝒫X\in \mathrm{SAlg}$$

Proof

Step	Hyp	Ref	Expression
1		0elpw	$$⊢\varnothing \in 𝒫X$$
2	1	a1i	$$⊢X\in V\to \varnothing \in 𝒫X$$
3		unipw	$$⊢\bigcup 𝒫X=X$$
4	3	difeq1i	$$⊢\bigcup 𝒫X\setminus y=X\setminus y$$
5	4	a1i	$$⊢X\in V\to \bigcup 𝒫X\setminus y=X\setminus y$$
6		difssd	$$⊢X\in V\to X\setminus y\subseteq X$$
7		difexg	$$⊢X\in V\to X\setminus y\in \mathrm{V}$$
8		elpwg	$$⊢X\setminus y\in \mathrm{V}\to \left(X\setminus y\in 𝒫X\leftrightarrow X\setminus y\subseteq X\right)$$
9	7 8	syl	$$⊢X\in V\to \left(X\setminus y\in 𝒫X\leftrightarrow X\setminus y\subseteq X\right)$$
10	6 9	mpbird	$$⊢X\in V\to X\setminus y\in 𝒫X$$
11	5 10	eqeltrd	$$⊢X\in V\to \bigcup 𝒫X\setminus y\in 𝒫X$$
12	11	adantr	$$⊢\left(X\in V\wedge y\in 𝒫X\right)\to \bigcup 𝒫X\setminus y\in 𝒫X$$
13	12	ralrimiva	$$⊢X\in V\to \forall y\in 𝒫X\bigcup 𝒫X\setminus y\in 𝒫X$$
14		elpwi	$$⊢y\in 𝒫𝒫X\to y\subseteq 𝒫X$$
15	14	unissd	$$⊢y\in 𝒫𝒫X\to \bigcup y\subseteq \bigcup 𝒫X$$
16	15 3	sseqtrdi	$$⊢y\in 𝒫𝒫X\to \bigcup y\subseteq X$$
17		vuniex	$$⊢\bigcup y\in \mathrm{V}$$
18	17	a1i	$$⊢y\in 𝒫𝒫X\to \bigcup y\in \mathrm{V}$$
19		elpwg	$$⊢\bigcup y\in \mathrm{V}\to \left(\bigcup y\in 𝒫X\leftrightarrow \bigcup y\subseteq X\right)$$
20	18 19	syl	$$⊢y\in 𝒫𝒫X\to \left(\bigcup y\in 𝒫X\leftrightarrow \bigcup y\subseteq X\right)$$
21	16 20	mpbird	$$⊢y\in 𝒫𝒫X\to \bigcup y\in 𝒫X$$
22	21	adantl	$$⊢\left(X\in V\wedge y\in 𝒫𝒫X\right)\to \bigcup y\in 𝒫X$$
23	22	a1d	$$⊢\left(X\in V\wedge y\in 𝒫𝒫X\right)\to \left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in 𝒫X\right)$$
24	23	ralrimiva	$$⊢X\in V\to \forall y\in 𝒫𝒫X\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in 𝒫X\right)$$
25	2 13 24	3jca	$$⊢X\in V\to \left(\varnothing \in 𝒫X\wedge \forall y\in 𝒫X\bigcup 𝒫X\setminus y\in 𝒫X\wedge \forall y\in 𝒫𝒫X\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in 𝒫X\right)\right)$$
26		pwexg	$$⊢X\in V\to 𝒫X\in \mathrm{V}$$
27		issal	$$⊢𝒫X\in \mathrm{V}\to \left(𝒫X\in \mathrm{SAlg}\leftrightarrow \left(\varnothing \in 𝒫X\wedge \forall y\in 𝒫X\bigcup 𝒫X\setminus y\in 𝒫X\wedge \forall y\in 𝒫𝒫X\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in 𝒫X\right)\right)\right)$$
28	26 27	syl	$$⊢X\in V\to \left(𝒫X\in \mathrm{SAlg}\leftrightarrow \left(\varnothing \in 𝒫X\wedge \forall y\in 𝒫X\bigcup 𝒫X\setminus y\in 𝒫X\wedge \forall y\in 𝒫𝒫X\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in 𝒫X\right)\right)\right)$$
29	25 28	mpbird	$$⊢X\in V\to 𝒫X\in \mathrm{SAlg}$$