Metamath Proof Explorer

Theorem iccmbl

Description: A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion iccmbl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 iccssre ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ⊆ ℝ
2 dfss4 ⊢ A B ⊆ ℝ ↔ ℝ ∖ ℝ ∖ A B = A B
3 1 2 sylib ⊢ A ∈ ℝ ∧ B ∈ ℝ → ℝ ∖ ℝ ∖ A B = A B
4 difreicc ⊢ A ∈ ℝ ∧ B ∈ ℝ → ℝ ∖ A B = −∞ A ∪ B +∞
5 ioombl ⊢ −∞ A ∈ dom ⁡ vol
6 ioombl ⊢ B +∞ ∈ dom ⁡ vol
7 unmbl ⊢ −∞ A ∈ dom ⁡ vol ∧ B +∞ ∈ dom ⁡ vol → −∞ A ∪ B +∞ ∈ dom ⁡ vol
8 5 6 7 mp2an ⊢ −∞ A ∪ B +∞ ∈ dom ⁡ vol
9 4 8 eqeltrdi ⊢ A ∈ ℝ ∧ B ∈ ℝ → ℝ ∖ A B ∈ dom ⁡ vol
10 cmmbl ⊢ ℝ ∖ A B ∈ dom ⁡ vol → ℝ ∖ ℝ ∖ A B ∈ dom ⁡ vol
11 9 10 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → ℝ ∖ ℝ ∖ A B ∈ dom ⁡ vol
12 3 11 eqeltrrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ dom ⁡ vol