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 ⊢ φ → O ∈ V
carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
difelcarsg.1 ⊢ φ → A ∈ toCaraSiga ⁡ M
Assertion difelcarsg ⊢ φ → O ∖ A ∈ toCaraSiga ⁡ M

Proof

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