Metamath Proof Explorer

Theorem carsgval

Description: Value of the Caratheodory sigma-Algebra construction function. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
Assertion carsgval ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) = { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 df-carsg ⊢ toCaraSiga = ( 𝑚 ∈ V ↦ { 𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀ 𝑒 ∈ 𝒫 ∪ dom 𝑚 ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 ) } )
4 simpr ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
5 4 dmeqd ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → dom 𝑚 = dom 𝑀 )
6 2 fdmd ⊢ ( 𝜑 → dom 𝑀 = 𝒫 𝑂 )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → dom 𝑀 = 𝒫 𝑂 )
8 5 7 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → dom 𝑚 = 𝒫 𝑂 )
9 8 unieqd ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → ∪ dom 𝑚 = ∪ 𝒫 𝑂 )
10 unipw ⊢ ∪ 𝒫 𝑂 = 𝑂
11 9 10 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → ∪ dom 𝑚 = 𝑂 )
12 11 pweqd ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → 𝒫 ∪ dom 𝑚 = 𝒫 𝑂 )
13 fveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) = ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) )
14 fveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) = ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) )
15 13 14 oveq12d ⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) )
16 fveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ 𝑒 ) = ( 𝑀 ‘ 𝑒 ) )
17 15 16 eqeq12d ⊢ ( 𝑚 = 𝑀 → ( ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 ) ↔ ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → ( ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 ) ↔ ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
19 12 18 raleqbidv ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑒 ∈ 𝒫 ∪ dom 𝑚 ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 ) ↔ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
20 12 19 rabeqbidv ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → { 𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀ 𝑒 ∈ 𝒫 ∪ dom 𝑚 ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 ) } = { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } )
21 1 pwexd ⊢ ( 𝜑 → 𝒫 𝑂 ∈ V )
22 fex ⊢ ( ( 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) ∧ 𝒫 𝑂 ∈ V ) → 𝑀 ∈ V )
23 2 21 22 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ V )
24 pwexg ⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V )
25 rabexg ⊢ ( 𝒫 𝑂 ∈ V → { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } ∈ V )
26 1 24 25 3syl ⊢ ( 𝜑 → { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } ∈ V )
27 3 20 23 26 fvmptd2 ⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) = { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } )