Metamath Proof Explorer

Theorem sigaval

Description: The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016)

Ref Expression
Assertion sigaval ( 𝑂 ∈ V → ( sigAlgebra ‘ 𝑂 ) = { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )

Proof

Step Hyp Ref Expression
1 df-rab ⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) } = { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) }
2 velpw ⊢ ( 𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂 )
3 2 anbi1i ⊢ ( ( 𝑠 ∈ 𝒫 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) ↔ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) )
4 3 abbii ⊢ { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) }
5 1 4 eqtri ⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) }
6 pwexg ⊢ ( 𝑂 ∈ V → 𝒫 𝑂 ∈ V )
7 pwexg ⊢ ( 𝒫 𝑂 ∈ V → 𝒫 𝒫 𝑂 ∈ V )
8 rabexg ⊢ ( 𝒫 𝒫 𝑂 ∈ V → { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) } ∈ V )
9 6 7 8 3syl ⊢ ( 𝑂 ∈ V → { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) } ∈ V )
10 5 9 eqeltrrid ⊢ ( 𝑂 ∈ V → { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } ∈ V )
11 pweq ⊢ ( 𝑜 = 𝑂 → 𝒫 𝑜 = 𝒫 𝑂 )
12 11 sseq2d ⊢ ( 𝑜 = 𝑂 → ( 𝑠 ⊆ 𝒫 𝑜 ↔ 𝑠 ⊆ 𝒫 𝑂 ) )
13 eleq1 ⊢ ( 𝑜 = 𝑂 → ( 𝑜 ∈ 𝑠 ↔ 𝑂 ∈ 𝑠 ) )
14 difeq1 ⊢ ( 𝑜 = 𝑂 → ( 𝑜 ∖ 𝑥 ) = ( 𝑂 ∖ 𝑥 ) )
15 14 eleq1d ⊢ ( 𝑜 = 𝑂 → ( ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ) )
16 15 ralbidv ⊢ ( 𝑜 = 𝑂 → ( ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ) )
17 13 16 3anbi12d ⊢ ( 𝑜 = 𝑂 → ( ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ↔ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) )
18 12 17 anbi12d ⊢ ( 𝑜 = 𝑂 → ( ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) ↔ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) ) )
19 18 abbidv ⊢ ( 𝑜 = 𝑂 → { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )
20 df-siga ⊢ sigAlgebra = ( 𝑜 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )
21 19 20 fvmptg ⊢ ( ( 𝑂 ∈ V ∧ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } ∈ V ) → ( sigAlgebra ‘ 𝑂 ) = { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )
22 10 21 mpdan ⊢ ( 𝑂 ∈ V → ( sigAlgebra ‘ 𝑂 ) = { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )