Metamath Proof Explorer


Theorem iccmbl

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

Ref Expression
Assertion iccmbl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 iccssre ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
2 dfss4 ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ↔ ( ℝ ∖ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) = ( 𝐴 [,] 𝐵 ) )
3 1 2 sylib ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) = ( 𝐴 [,] 𝐵 ) )
4 difreicc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) = ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) )
5 ioombl ( -∞ (,) 𝐴 ) ∈ dom vol
6 ioombl ( 𝐵 (,) +∞ ) ∈ dom vol
7 unmbl ( ( ( -∞ (,) 𝐴 ) ∈ dom vol ∧ ( 𝐵 (,) +∞ ) ∈ dom vol ) → ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) ∈ dom vol )
8 5 6 7 mp2an ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) ∈ dom vol
9 4 8 eqeltrdi ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ∈ dom vol )
10 cmmbl ( ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ∈ dom vol → ( ℝ ∖ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ∈ dom vol )
11 9 10 syl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ∈ dom vol )
12 3 11 eqeltrrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ dom vol )