Metamath Proof Explorer

Theorem inmbl

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

Ref Expression
Assertion inmbl ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → A ∩ B ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 difundi ⊢ ℝ ∖ ℝ ∖ A ∪ ℝ ∖ B = ℝ ∖ ℝ ∖ A ∩ ℝ ∖ ℝ ∖ B
2 mblss ⊢ A ∈ dom ⁡ vol → A ⊆ ℝ
3 dfss4 ⊢ A ⊆ ℝ ↔ ℝ ∖ ℝ ∖ A = A
4 2 3 sylib ⊢ A ∈ dom ⁡ vol → ℝ ∖ ℝ ∖ A = A
5 mblss ⊢ B ∈ dom ⁡ vol → B ⊆ ℝ
6 dfss4 ⊢ B ⊆ ℝ ↔ ℝ ∖ ℝ ∖ B = B
7 5 6 sylib ⊢ B ∈ dom ⁡ vol → ℝ ∖ ℝ ∖ B = B
8 4 7 ineqan12d ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → ℝ ∖ ℝ ∖ A ∩ ℝ ∖ ℝ ∖ B = A ∩ B
9 1 8 eqtrid ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → ℝ ∖ ℝ ∖ A ∪ ℝ ∖ B = A ∩ B
10 cmmbl ⊢ A ∈ dom ⁡ vol → ℝ ∖ A ∈ dom ⁡ vol
11 cmmbl ⊢ B ∈ dom ⁡ vol → ℝ ∖ B ∈ dom ⁡ vol
12 unmbl ⊢ ℝ ∖ A ∈ dom ⁡ vol ∧ ℝ ∖ B ∈ dom ⁡ vol → ℝ ∖ A ∪ ℝ ∖ B ∈ dom ⁡ vol
13 10 11 12 syl2an ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → ℝ ∖ A ∪ ℝ ∖ B ∈ dom ⁡ vol
14 cmmbl ⊢ ℝ ∖ A ∪ ℝ ∖ B ∈ dom ⁡ vol → ℝ ∖ ℝ ∖ A ∪ ℝ ∖ B ∈ dom ⁡ vol
15 13 14 syl ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → ℝ ∖ ℝ ∖ A ∪ ℝ ∖ B ∈ dom ⁡ vol
16 9 15 eqeltrrd ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → A ∩ B ∈ dom ⁡ vol