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 ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ ( sigAlgebra ‘ 𝑂 ) )

Proof

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