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 ∈ 𝒫 O O ∖ 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 ∈ 𝒫 𝒫 O x ≼ ω → ⋃ x ∈ 𝒫 O
18 2 7 17 3jca ⊢ O ∈ V → O ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 O O ∖ x ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 𝒫 O x ≼ ω → ⋃ x ∈ 𝒫 O
19 pwexg ⊢ O ∈ V → 𝒫 O ∈ V
20 issiga ⊢ 𝒫 O ∈ V → 𝒫 O ∈ sigAlgebra ⁡ O ↔ 𝒫 O ⊆ 𝒫 O ∧ O ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 O O ∖ x ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 𝒫 O x ≼ ω → ⋃ x ∈ 𝒫 O
21 19 20 syl ⊢ O ∈ V → 𝒫 O ∈ sigAlgebra ⁡ O ↔ 𝒫 O ⊆ 𝒫 O ∧ O ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 O O ∖ x ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 𝒫 O x ≼ ω → ⋃ x ∈ 𝒫 O
22 1 18 21 mpbir2and ⊢ O ∈ V → 𝒫 O ∈ sigAlgebra ⁡ O