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