This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difmbl

Description: A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion difmbl ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∖ 𝐵 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 indif2 ⊢ ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) = ( ( 𝐴 ∩ ℝ ) ∖ 𝐵 )
2 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
3 dfss2 ⊢ ( 𝐴 ⊆ ℝ ↔ ( 𝐴 ∩ ℝ ) = 𝐴 )
4 2 3 sylib ⊢ ( 𝐴 ∈ dom vol → ( 𝐴 ∩ ℝ ) = 𝐴 )
5 4 difeq1d ⊢ ( 𝐴 ∈ dom vol → ( ( 𝐴 ∩ ℝ ) ∖ 𝐵 ) = ( 𝐴 ∖ 𝐵 ) )
6 1 5 eqtrid ⊢ ( 𝐴 ∈ dom vol → ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 ) )
8 cmmbl ⊢ ( 𝐵 ∈ dom vol → ( ℝ ∖ 𝐵 ) ∈ dom vol )
9 inmbl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( ℝ ∖ 𝐵 ) ∈ dom vol ) → ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) ∈ dom vol )
10 8 9 sylan2 ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) ∈ dom vol )
11 7 10 eqeltrrd ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∖ 𝐵 ) ∈ dom vol )