This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )