# Metamath Proof Explorer

## Theorem inmbl

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

Ref Expression
Assertion inmbl ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to {A}\cap {B}\in \mathrm{dom}vol$

### Proof

Step Hyp Ref Expression
1 difundi ${⊢}ℝ\setminus \left(\left(ℝ\setminus {A}\right)\cup \left(ℝ\setminus {B}\right)\right)=\left(ℝ\setminus \left(ℝ\setminus {A}\right)\right)\cap \left(ℝ\setminus \left(ℝ\setminus {B}\right)\right)$
2 mblss ${⊢}{A}\in \mathrm{dom}vol\to {A}\subseteq ℝ$
3 dfss4 ${⊢}{A}\subseteq ℝ↔ℝ\setminus \left(ℝ\setminus {A}\right)={A}$
4 2 3 sylib ${⊢}{A}\in \mathrm{dom}vol\to ℝ\setminus \left(ℝ\setminus {A}\right)={A}$
5 mblss ${⊢}{B}\in \mathrm{dom}vol\to {B}\subseteq ℝ$
6 dfss4 ${⊢}{B}\subseteq ℝ↔ℝ\setminus \left(ℝ\setminus {B}\right)={B}$
7 5 6 sylib ${⊢}{B}\in \mathrm{dom}vol\to ℝ\setminus \left(ℝ\setminus {B}\right)={B}$
8 4 7 ineqan12d ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to \left(ℝ\setminus \left(ℝ\setminus {A}\right)\right)\cap \left(ℝ\setminus \left(ℝ\setminus {B}\right)\right)={A}\cap {B}$
9 1 8 syl5eq ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to ℝ\setminus \left(\left(ℝ\setminus {A}\right)\cup \left(ℝ\setminus {B}\right)\right)={A}\cap {B}$
10 cmmbl ${⊢}{A}\in \mathrm{dom}vol\to ℝ\setminus {A}\in \mathrm{dom}vol$
11 cmmbl ${⊢}{B}\in \mathrm{dom}vol\to ℝ\setminus {B}\in \mathrm{dom}vol$
12 unmbl ${⊢}\left(ℝ\setminus {A}\in \mathrm{dom}vol\wedge ℝ\setminus {B}\in \mathrm{dom}vol\right)\to \left(ℝ\setminus {A}\right)\cup \left(ℝ\setminus {B}\right)\in \mathrm{dom}vol$
13 10 11 12 syl2an ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to \left(ℝ\setminus {A}\right)\cup \left(ℝ\setminus {B}\right)\in \mathrm{dom}vol$
14 cmmbl ${⊢}\left(ℝ\setminus {A}\right)\cup \left(ℝ\setminus {B}\right)\in \mathrm{dom}vol\to ℝ\setminus \left(\left(ℝ\setminus {A}\right)\cup \left(ℝ\setminus {B}\right)\right)\in \mathrm{dom}vol$
15 13 14 syl ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to ℝ\setminus \left(\left(ℝ\setminus {A}\right)\cup \left(ℝ\setminus {B}\right)\right)\in \mathrm{dom}vol$
16 9 15 eqeltrrd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to {A}\cap {B}\in \mathrm{dom}vol$