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 )