This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )