Metamath Proof Explorer

Theorem elcarsg

Description: Property of being a Caratheodory measurable set. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
Assertion elcarsg ( 𝜑 → ( 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 1 2 carsgval ⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) = { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } )
4 3 eleq2d ⊢ ( 𝜑 → ( 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ 𝐴 ∈ { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } ) )
5 ineq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑒 ∩ 𝑎 ) = ( 𝑒 ∩ 𝐴 ) )
6 5 fveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) = ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) )
7 difeq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑒 ∖ 𝑎 ) = ( 𝑒 ∖ 𝐴 ) )
8 7 fveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) = ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) )
9 6 8 oveq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
10 9 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
11 10 ralbidv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
12 11 elrab ⊢ ( 𝐴 ∈ { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } ↔ ( 𝐴 ∈ 𝒫 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
13 elex ⊢ ( 𝐴 ∈ 𝒫 𝑂 → 𝐴 ∈ V )
14 13 a1i ⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝑂 → 𝐴 ∈ V ) )
15 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝑂 ) → 𝑂 ∈ 𝑉 )
16 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ⊆ 𝑂 )
17 15 16 ssexd ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ∈ V )
18 17 ex ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝑂 → 𝐴 ∈ V ) )
19 elpwg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝑂 ↔ 𝐴 ⊆ 𝑂 ) )
20 19 a1i ⊢ ( 𝜑 → ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝑂 ↔ 𝐴 ⊆ 𝑂 ) ) )
21 14 18 20 pm5.21ndd ⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝑂 ↔ 𝐴 ⊆ 𝑂 ) )
22 21 anbi1d ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝒫 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ↔ ( 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
23 12 22 syl5bb ⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } ↔ ( 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
24 4 23 bitrd ⊢ ( 𝜑 → ( 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )