Metamath Proof Explorer

Theorem caragenval

Description: The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion caragenval ( 𝑂 ∈ OutMeas → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑂 ∈ OutMeas → 𝑂 ∈ OutMeas )
2 dmexg ⊢ ( 𝑂 ∈ OutMeas → dom 𝑂 ∈ V )
3 2 uniexd ⊢ ( 𝑂 ∈ OutMeas → ∪ dom 𝑂 ∈ V )
4 3 pwexd ⊢ ( 𝑂 ∈ OutMeas → 𝒫 ∪ dom 𝑂 ∈ V )
5 rabexg ⊢ ( 𝒫 ∪ dom 𝑂 ∈ V → { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ∈ V )
6 4 5 syl ⊢ ( 𝑂 ∈ OutMeas → { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ∈ V )
7 dmeq ⊢ ( 𝑜 = 𝑂 → dom 𝑜 = dom 𝑂 )
8 7 unieqd ⊢ ( 𝑜 = 𝑂 → ∪ dom 𝑜 = ∪ dom 𝑂 )
9 8 pweqd ⊢ ( 𝑜 = 𝑂 → 𝒫 ∪ dom 𝑜 = 𝒫 ∪ dom 𝑂 )
10 9 raleqdv ⊢ ( 𝑜 = 𝑂 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ) )
11 fveq1 ⊢ ( 𝑜 = 𝑂 → ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) = ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) )
12 fveq1 ⊢ ( 𝑜 = 𝑂 → ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) = ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) )
13 11 12 oveq12d ⊢ ( 𝑜 = 𝑂 → ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) )
14 fveq1 ⊢ ( 𝑜 = 𝑂 → ( 𝑜 ‘ 𝑎 ) = ( 𝑂 ‘ 𝑎 ) )
15 13 14 eqeq12d ⊢ ( 𝑜 = 𝑂 → ( ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ↔ ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
16 15 ralbidv ⊢ ( 𝑜 = 𝑂 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
17 10 16 bitrd ⊢ ( 𝑜 = 𝑂 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
18 9 17 rabeqbidv ⊢ ( 𝑜 = 𝑂 → { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
19 df-caragen ⊢ CaraGen = ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } )
20 18 19 fvmptg ⊢ ( ( 𝑂 ∈ OutMeas ∧ { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ∈ V ) → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
21 1 6 20 syl2anc ⊢ ( 𝑂 ∈ OutMeas → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )