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∈V→𝒫O∈sigAlgebra⁡O

Proof

Step Hyp Ref Expression
1 ssidd ⊢O∈V→𝒫O⊆𝒫O
2 pwidg ⊢O∈V→O∈𝒫O
3 difss ⊢O∖x⊆O
4 elpw2g ⊢O∈V→O∖x∈𝒫O↔O∖x⊆O
5 3 4 mpbiri ⊢O∈V→O∖x∈𝒫O
6 5 a1d ⊢O∈V→x∈𝒫O→O∖x∈𝒫O
7 6 ralrimiv ⊢O∈V→∀x∈𝒫OO∖x∈𝒫O
8 sspwuni ⊢x⊆𝒫O↔⋃x⊆O
9 vuniex ⊢⋃x∈V
10 9 elpw ⊢⋃x∈𝒫O↔⋃x⊆O
11 8 10 bitr4i ⊢x⊆𝒫O↔⋃x∈𝒫O
12 11 biimpi ⊢x⊆𝒫O→⋃x∈𝒫O
13 12 a1d ⊢x⊆𝒫O→x≼ω→⋃x∈𝒫O
14 elpwi ⊢x∈𝒫𝒫O→x⊆𝒫O
15 14 imim1i ⊢x⊆𝒫O→x≼ω→⋃x∈𝒫O→x∈𝒫𝒫O→x≼ω→⋃x∈𝒫O
16 13 15 mp1i ⊢O∈V→x∈𝒫𝒫O→x≼ω→⋃x∈𝒫O
17 16 ralrimiv ⊢O∈V→∀x∈𝒫𝒫Ox≼ω→⋃x∈𝒫O
18 2 7 17 3jca ⊢O∈V→O∈𝒫O∧∀x∈𝒫OO∖x∈𝒫O∧∀x∈𝒫𝒫Ox≼ω→⋃x∈𝒫O
19 pwexg ⊢O∈V→𝒫O∈V
20 issiga ⊢𝒫O∈V→𝒫O∈sigAlgebra⁡O↔𝒫O⊆𝒫O∧O∈𝒫O∧∀x∈𝒫OO∖x∈𝒫O∧∀x∈𝒫𝒫Ox≼ω→⋃x∈𝒫O
21 19 20 syl ⊢O∈V→𝒫O∈sigAlgebra⁡O↔𝒫O⊆𝒫O∧O∈𝒫O∧∀x∈𝒫OO∖x∈𝒫O∧∀x∈𝒫𝒫Ox≼ω→⋃x∈𝒫O
22 1 18 21 mpbir2and ⊢O∈V→𝒫O∈sigAlgebra⁡O