Theorem icombl1

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

	Ref	Expression
Assertion	icombl1	$$⊢A\in ℝ\to \left[A,\mathrm{+\infty }\right)\in \mathrm{dom}vol$$

Proof

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