# Metamath Proof Explorer

## Theorem pwsiga

Description: Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016) (Revised by Thierry Arnoux, 24-Oct-2016)

Ref Expression
Assertion pwsiga ${⊢}{O}\in {V}\to 𝒫{O}\in \mathrm{sigAlgebra}\left({O}\right)$

### Proof

Step Hyp Ref Expression
1 ssidd ${⊢}{O}\in {V}\to 𝒫{O}\subseteq 𝒫{O}$
2 pwidg ${⊢}{O}\in {V}\to {O}\in 𝒫{O}$
3 difss ${⊢}{O}\setminus {x}\subseteq {O}$
4 elpw2g ${⊢}{O}\in {V}\to \left({O}\setminus {x}\in 𝒫{O}↔{O}\setminus {x}\subseteq {O}\right)$
5 3 4 mpbiri ${⊢}{O}\in {V}\to {O}\setminus {x}\in 𝒫{O}$
6 5 a1d ${⊢}{O}\in {V}\to \left({x}\in 𝒫{O}\to {O}\setminus {x}\in 𝒫{O}\right)$
7 6 ralrimiv ${⊢}{O}\in {V}\to \forall {x}\in 𝒫{O}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in 𝒫{O}$
8 sspwuni ${⊢}{x}\subseteq 𝒫{O}↔\bigcup {x}\subseteq {O}$
9 vuniex ${⊢}\bigcup {x}\in \mathrm{V}$
10 9 elpw ${⊢}\bigcup {x}\in 𝒫{O}↔\bigcup {x}\subseteq {O}$
11 8 10 bitr4i ${⊢}{x}\subseteq 𝒫{O}↔\bigcup {x}\in 𝒫{O}$
12 11 biimpi ${⊢}{x}\subseteq 𝒫{O}\to \bigcup {x}\in 𝒫{O}$
13 12 a1d ${⊢}{x}\subseteq 𝒫{O}\to \left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in 𝒫{O}\right)$
14 elpwi ${⊢}{x}\in 𝒫𝒫{O}\to {x}\subseteq 𝒫{O}$
15 14 imim1i ${⊢}\left({x}\subseteq 𝒫{O}\to \left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in 𝒫{O}\right)\right)\to \left({x}\in 𝒫𝒫{O}\to \left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in 𝒫{O}\right)\right)$
16 13 15 mp1i ${⊢}{O}\in {V}\to \left({x}\in 𝒫𝒫{O}\to \left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in 𝒫{O}\right)\right)$
17 16 ralrimiv ${⊢}{O}\in {V}\to \forall {x}\in 𝒫𝒫{O}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in 𝒫{O}\right)$
18 2 7 17 3jca ${⊢}{O}\in {V}\to \left({O}\in 𝒫{O}\wedge \forall {x}\in 𝒫{O}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in 𝒫{O}\wedge \forall {x}\in 𝒫𝒫{O}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in 𝒫{O}\right)\right)$
19 pwexg ${⊢}{O}\in {V}\to 𝒫{O}\in \mathrm{V}$
20 issiga ${⊢}𝒫{O}\in \mathrm{V}\to \left(𝒫{O}\in \mathrm{sigAlgebra}\left({O}\right)↔\left(𝒫{O}\subseteq 𝒫{O}\wedge \left({O}\in 𝒫{O}\wedge \forall {x}\in 𝒫{O}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in 𝒫{O}\wedge \forall {x}\in 𝒫𝒫{O}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in 𝒫{O}\right)\right)\right)\right)$
21 19 20 syl ${⊢}{O}\in {V}\to \left(𝒫{O}\in \mathrm{sigAlgebra}\left({O}\right)↔\left(𝒫{O}\subseteq 𝒫{O}\wedge \left({O}\in 𝒫{O}\wedge \forall {x}\in 𝒫{O}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in 𝒫{O}\wedge \forall {x}\in 𝒫𝒫{O}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in 𝒫{O}\right)\right)\right)\right)$
22 1 18 21 mpbir2and ${⊢}{O}\in {V}\to 𝒫{O}\in \mathrm{sigAlgebra}\left({O}\right)$