Theorem icombl1

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

	Ref	Expression
Assertion	icombl1	|- ( A e. RR -> ( A [,) +oo ) e. dom vol )

Proof

Step	Hyp	Ref	Expression
1		rexr	|- ( A e. RR -> A e. RR* )
2		pnfxr	|- +oo e. RR*
3	2	a1i	|- ( A e. RR -> +oo e. RR* )
4		ltpnf	|- ( A e. RR -> A < +oo )
5		snunioo	|- ( ( A e. RR* /\ +oo e. RR* /\ A < +oo ) -> ( { A } u. ( A (,) +oo ) ) = ( A [,) +oo ) )
6	1 3 4 5	syl3anc	|- ( A e. RR -> ( { A } u. ( A (,) +oo ) ) = ( A [,) +oo ) )
7		snssi	|- ( A e. RR -> { A } C_ RR )
8		ovolsn	|- ( A e. RR -> ( vol* ` { A } ) = 0 )
9		nulmbl	|- ( ( { A } C_ RR /\ ( vol* ` { A } ) = 0 ) -> { A } e. dom vol )
10	7 8 9	syl2anc	|- ( A e. RR -> { A } e. dom vol )
11		ioombl1	|- ( A e. RR* -> ( A (,) +oo ) e. dom vol )
12	1 11	syl	|- ( A e. RR -> ( A (,) +oo ) e. dom vol )
13		unmbl	|- ( ( { A } e. dom vol /\ ( A (,) +oo ) e. dom vol ) -> ( { A } u. ( A (,) +oo ) ) e. dom vol )
14	10 12 13	syl2anc	|- ( A e. RR -> ( { A } u. ( A (,) +oo ) ) e. dom vol )
15	6 14	eqeltrrd	|- ( A e. RR -> ( A [,) +oo ) e. dom vol )