# Metamath Proof Explorer

## 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}↔{X}\setminus {y}\subseteq {X}\right)$
9 7 8 syl ${⊢}{X}\in {V}\to \left({X}\setminus {y}\in 𝒫{X}↔{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}\phantom{\rule{.4em}{0ex}}\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}↔\bigcup {y}\subseteq {X}\right)$
20 18 19 syl ${⊢}{y}\in 𝒫𝒫{X}\to \left(\bigcup {y}\in 𝒫{X}↔\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\bigcup 𝒫{X}\setminus {y}\in 𝒫{X}\wedge \forall {y}\in 𝒫𝒫{X}\phantom{\rule{.4em}{0ex}}\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}↔\left(\varnothing \in 𝒫{X}\wedge \forall {y}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\bigcup 𝒫{X}\setminus {y}\in 𝒫{X}\wedge \forall {y}\in 𝒫𝒫{X}\phantom{\rule{.4em}{0ex}}\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}↔\left(\varnothing \in 𝒫{X}\wedge \forall {y}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\bigcup 𝒫{X}\setminus {y}\in 𝒫{X}\wedge \forall {y}\in 𝒫𝒫{X}\phantom{\rule{.4em}{0ex}}\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}$