iccmbl

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

		Ref	Expression
	Assertion	iccmbl	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in dom vol$

Step	Hyp	Ref	Expression
1		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
2		dfss4	$⊢ [A, B] \subseteq ℝ \leftrightarrow ℝ ∖ (ℝ ∖ [A, B]) = [A, B]$
3	1 2	sylib	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ (ℝ ∖ [A, B]) = [A, B]$
4		difreicc	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ [A, B] = (−∞, A) \cup (B, +∞)$
5		ioombl	$⊢ (−∞, A) \in dom vol$
6		ioombl	$⊢ (B, +∞) \in dom vol$
7		unmbl	$⊢ ((−∞, A) \in dom vol \land (B, +∞) \in dom vol) \to (−∞, A) \cup (B, +∞) \in dom vol$
8	5 6 7	mp2an	$⊢ (−∞, A) \cup (B, +∞) \in dom vol$
9	4 8	eqeltrdi	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ [A, B] \in dom vol$
10		cmmbl	$⊢ ℝ ∖ [A, B] \in dom vol \to ℝ ∖ (ℝ ∖ [A, B]) \in dom vol$
11	9 10	syl	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ (ℝ ∖ [A, B]) \in dom vol$
12	3 11	eqeltrrd	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in dom vol$

Metamath Proof Explorer