Metamath Proof Explorer

Theorem cmmbl

Description: The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion cmmbl ( 𝐴 ∈ dom vol → ( ℝ ∖ 𝐴 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 difssd ⊢ ( 𝐴 ∈ dom vol → ( ℝ ∖ 𝐴 ) ⊆ ℝ )
2 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
3 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
4 ovolsscl ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
5 3 4 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
6 5 3adant1 ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ )
7 6 recnd ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℂ )
8 difss ⊢ ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥
9 ovolsscl ⊢ ( ( ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
10 8 9 mp3an1 ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
11 10 3adant1 ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℂ )
13 7 12 addcomd ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ) )
14 mblsplit ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
15 indifcom ⊢ ( ℝ ∩ ( 𝑥 ∖ 𝐴 ) ) = ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) )
16 simp2 ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → 𝑥 ⊆ ℝ )
17 16 ssdifssd ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∖ 𝐴 ) ⊆ ℝ )
18 sseqin2 ⊢ ( ( 𝑥 ∖ 𝐴 ) ⊆ ℝ ↔ ( ℝ ∩ ( 𝑥 ∖ 𝐴 ) ) = ( 𝑥 ∖ 𝐴 ) )
19 17 18 sylib ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ℝ ∩ ( 𝑥 ∖ 𝐴 ) ) = ( 𝑥 ∖ 𝐴 ) )
20 15 19 eqtr3id ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) = ( 𝑥 ∖ 𝐴 ) )
21 20 fveq2d ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) = ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) )
22 difin ⊢ ( 𝑥 ∖ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) = ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) )
23 20 difeq2d ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∖ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) = ( 𝑥 ∖ ( 𝑥 ∖ 𝐴 ) ) )
24 22 23 eqtr3id ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) = ( 𝑥 ∖ ( 𝑥 ∖ 𝐴 ) ) )
25 dfin4 ⊢ ( 𝑥 ∩ 𝐴 ) = ( 𝑥 ∖ ( 𝑥 ∖ 𝐴 ) )
26 24 25 eqtr4di ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) = ( 𝑥 ∩ 𝐴 ) )
27 26 fveq2d ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) ) = ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) )
28 21 27 oveq12d ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( vol* ‘ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) ) ) = ( ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ) )
29 13 14 28 3eqtr4d ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) ) ) )
30 29 3expia ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) ) ) ) )
31 2 30 sylan2 ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝒫 ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) ) ) ) )
32 31 ralrimiva ⊢ ( 𝐴 ∈ dom vol → ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) ) ) ) )
33 ismbl ⊢ ( ( ℝ ∖ 𝐴 ) ∈ dom vol ↔ ( ( ℝ ∖ 𝐴 ) ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ ( ℝ ∖ 𝐴 ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( ℝ ∖ 𝐴 ) ) ) ) ) ) )
34 1 32 33 sylanbrc ⊢ ( 𝐴 ∈ dom vol → ( ℝ ∖ 𝐴 ) ∈ dom vol )