Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  inmbl Structured version   Visualization version   GIF version

Theorem inmbl 23356
 Description: An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
Assertion
Ref Expression
inmbl ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴𝐵) ∈ dom vol)

Proof of Theorem inmbl
StepHypRef Expression
1 difundi 3912 . . 3 (ℝ ∖ ((ℝ ∖ 𝐴) ∪ (ℝ ∖ 𝐵))) = ((ℝ ∖ (ℝ ∖ 𝐴)) ∩ (ℝ ∖ (ℝ ∖ 𝐵)))
2 mblss 23345 . . . . 5 (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
3 dfss4 3891 . . . . 5 (𝐴 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝐴)) = 𝐴)
42, 3sylib 208 . . . 4 (𝐴 ∈ dom vol → (ℝ ∖ (ℝ ∖ 𝐴)) = 𝐴)
5 mblss 23345 . . . . 5 (𝐵 ∈ dom vol → 𝐵 ⊆ ℝ)
6 dfss4 3891 . . . . 5 (𝐵 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝐵)) = 𝐵)
75, 6sylib 208 . . . 4 (𝐵 ∈ dom vol → (ℝ ∖ (ℝ ∖ 𝐵)) = 𝐵)
84, 7ineqan12d 3849 . . 3 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → ((ℝ ∖ (ℝ ∖ 𝐴)) ∩ (ℝ ∖ (ℝ ∖ 𝐵))) = (𝐴𝐵))
91, 8syl5eq 2697 . 2 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (ℝ ∖ ((ℝ ∖ 𝐴) ∪ (ℝ ∖ 𝐵))) = (𝐴𝐵))
10 cmmbl 23348 . . . 4 (𝐴 ∈ dom vol → (ℝ ∖ 𝐴) ∈ dom vol)
11 cmmbl 23348 . . . 4 (𝐵 ∈ dom vol → (ℝ ∖ 𝐵) ∈ dom vol)
12 unmbl 23351 . . . 4 (((ℝ ∖ 𝐴) ∈ dom vol ∧ (ℝ ∖ 𝐵) ∈ dom vol) → ((ℝ ∖ 𝐴) ∪ (ℝ ∖ 𝐵)) ∈ dom vol)
1310, 11, 12syl2an 493 . . 3 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → ((ℝ ∖ 𝐴) ∪ (ℝ ∖ 𝐵)) ∈ dom vol)
14 cmmbl 23348 . . 3 (((ℝ ∖ 𝐴) ∪ (ℝ ∖ 𝐵)) ∈ dom vol → (ℝ ∖ ((ℝ ∖ 𝐴) ∪ (ℝ ∖ 𝐵))) ∈ dom vol)
1513, 14syl 17 . 2 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (ℝ ∖ ((ℝ ∖ 𝐴) ∪ (ℝ ∖ 𝐵))) ∈ dom vol)
169, 15eqeltrrd 2731 1 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴𝐵) ∈ dom vol)