Metamath Proof Explorer

Theorem difelcarsg

Description: The Caratheodory measurable sets are closed under complement. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
difelcarsg.1 ⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
Assertion difelcarsg ( 𝜑 → ( 𝑂 ∖ 𝐴 ) ∈ ( toCaraSiga ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 difelcarsg.1 ⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
4 difssd ⊢ ( 𝜑 → ( 𝑂 ∖ 𝐴 ) ⊆ 𝑂 )
5 indif2 ⊢ ( 𝑒 ∩ ( 𝑂 ∖ 𝐴 ) ) = ( ( 𝑒 ∩ 𝑂 ) ∖ 𝐴 )
6 elpwi ⊢ ( 𝑒 ∈ 𝒫 𝑂 → 𝑒 ⊆ 𝑂 )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑒 ⊆ 𝑂 )
8 df-ss ⊢ ( 𝑒 ⊆ 𝑂 ↔ ( 𝑒 ∩ 𝑂 ) = 𝑒 )
9 7 8 sylib ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ 𝑂 ) = 𝑒 )
10 9 difeq1d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑒 ∩ 𝑂 ) ∖ 𝐴 ) = ( 𝑒 ∖ 𝐴 ) )
11 5 10 syl5eq ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ ( 𝑂 ∖ 𝐴 ) ) = ( 𝑒 ∖ 𝐴 ) )
12 11 fveq2d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ ( 𝑂 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) )
13 difdif2 ⊢ ( 𝑒 ∖ ( 𝑂 ∖ 𝐴 ) ) = ( ( 𝑒 ∖ 𝑂 ) ∪ ( 𝑒 ∩ 𝐴 ) )
14 ssdif0 ⊢ ( 𝑒 ⊆ 𝑂 ↔ ( 𝑒 ∖ 𝑂 ) = ∅ )
15 7 14 sylib ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∖ 𝑂 ) = ∅ )
16 15 uneq1d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑒 ∖ 𝑂 ) ∪ ( 𝑒 ∩ 𝐴 ) ) = ( ∅ ∪ ( 𝑒 ∩ 𝐴 ) ) )
17 uncom ⊢ ( ( 𝑒 ∩ 𝐴 ) ∪ ∅ ) = ( ∅ ∪ ( 𝑒 ∩ 𝐴 ) )
18 un0 ⊢ ( ( 𝑒 ∩ 𝐴 ) ∪ ∅ ) = ( 𝑒 ∩ 𝐴 )
19 17 18 eqtr3i ⊢ ( ∅ ∪ ( 𝑒 ∩ 𝐴 ) ) = ( 𝑒 ∩ 𝐴 )
20 16 19 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑒 ∖ 𝑂 ) ∪ ( 𝑒 ∩ 𝐴 ) ) = ( 𝑒 ∩ 𝐴 ) )
21 13 20 syl5eq ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∖ ( 𝑂 ∖ 𝐴 ) ) = ( 𝑒 ∩ 𝐴 ) )
22 21 fveq2d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ ( 𝑂 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) )
23 12 22 oveq12d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝑂 ∖ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ( 𝑂 ∖ 𝐴 ) ) ) ) = ( ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ) )
24 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
25 2 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑒 ∈ 𝒫 𝑂 )
27 26 elpwdifcl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∖ 𝐴 ) ∈ 𝒫 𝑂 )
28 25 27 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
29 24 28 sseldi ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ∈ ℝ* )
30 26 elpwincl1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ 𝐴 ) ∈ 𝒫 𝑂 )
31 25 30 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
32 24 31 sseldi ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ∈ ℝ* )
33 xaddcom ⊢ ( ( ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ∈ ℝ* ) → ( ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
34 29 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) ) = ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) )
35 1 2 elcarsg ⊢ ( 𝜑 → ( 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
36 3 35 mpbid ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
37 36 simprd ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
38 37 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
39 23 34 38 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝑂 ∖ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ( 𝑂 ∖ 𝐴 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) )
40 39 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝑂 ∖ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ( 𝑂 ∖ 𝐴 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) )
41 4 40 jca ⊢ ( 𝜑 → ( ( 𝑂 ∖ 𝐴 ) ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝑂 ∖ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ( 𝑂 ∖ 𝐴 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
42 1 2 elcarsg ⊢ ( 𝜑 → ( ( 𝑂 ∖ 𝐴 ) ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ( 𝑂 ∖ 𝐴 ) ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ( 𝑂 ∖ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ( 𝑂 ∖ 𝐴 ) ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
43 41 42 mpbird ⊢ ( 𝜑 → ( 𝑂 ∖ 𝐴 ) ∈ ( toCaraSiga ‘ 𝑀 ) )