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 )