icombl1

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

		Ref	Expression
	Assertion	icombl1	$⊢ A \in ℝ \to [A, +∞) \in dom vol$

Step	Hyp	Ref	Expression
1		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3	2	a1i	$⊢ A \in ℝ \to +∞ \in ℝ^{*}$
4		ltpnf	$⊢ A \in ℝ \to A < +∞$
5		snunioo	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{} \land A < +∞) \to \{A\} \cup (A, +∞) = [A, +∞)$
6	1 3 4 5	syl3anc	$⊢ A \in ℝ \to \{A\} \cup (A, +∞) = [A, +∞)$
7		snssi	$⊢ A \in ℝ \to \{A\} \subseteq ℝ$
8		ovolsn	$⊢ A \in ℝ \to {vol}^{*} (\{A\}) = 0$
9		nulmbl	$⊢ (\{A\} \subseteq ℝ \land {vol}^{*} (\{A\}) = 0) \to \{A\} \in dom vol$
10	7 8 9	syl2anc	$⊢ A \in ℝ \to \{A\} \in dom vol$
11		ioombl1	$⊢ A \in ℝ^{*} \to (A, +∞) \in dom vol$
12	1 11	syl	$⊢ A \in ℝ \to (A, +∞) \in dom vol$
13		unmbl	$⊢ (\{A\} \in dom vol \land (A, +∞) \in dom vol) \to \{A\} \cup (A, +∞) \in dom vol$
14	10 12 13	syl2anc	$⊢ A \in ℝ \to \{A\} \cup (A, +∞) \in dom vol$
15	6 14	eqeltrrd	$⊢ A \in ℝ \to [A, +∞) \in dom vol$

Metamath Proof Explorer