Metamath Proof Explorer

Theorem ovolre

Description: The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion ovolre 
|- ( vol* ` RR ) = +oo

Proof

Step Hyp Ref Expression
1 ssid 
 |-  RR C_ RR
2 ovolcl 
 |-  ( RR C_ RR -> ( vol* ` RR ) e. RR* )
3 1 2 ax-mp 
 |-  ( vol* ` RR ) e. RR*
4 pnfge 
 |-  ( ( vol* ` RR ) e. RR* -> ( vol* ` RR ) <_ +oo )
5 3 4 ax-mp 
 |-  ( vol* ` RR ) <_ +oo
6 0re 
 |-  0 e. RR
7 ovolicopnf 
 |-  ( 0 e. RR -> ( vol* ` ( 0 [,) +oo ) ) = +oo )
8 6 7 ax-mp 
 |-  ( vol* ` ( 0 [,) +oo ) ) = +oo
9 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
10 ovolss 
 |-  ( ( ( 0 [,) +oo ) C_ RR /\ RR C_ RR ) -> ( vol* ` ( 0 [,) +oo ) ) <_ ( vol* ` RR ) )
11 9 1 10 mp2an 
 |-  ( vol* ` ( 0 [,) +oo ) ) <_ ( vol* ` RR )
12 8 11 eqbrtrri 
 |-  +oo <_ ( vol* ` RR )
13 pnfxr 
 |-  +oo e. RR*
14 xrletri3 
 |-  ( ( ( vol* ` RR ) e. RR* /\ +oo e. RR* ) -> ( ( vol* ` RR ) = +oo <-> ( ( vol* ` RR ) <_ +oo /\ +oo <_ ( vol* ` RR ) ) ) )
15 3 13 14 mp2an 
 |-  ( ( vol* ` RR ) = +oo <-> ( ( vol* ` RR ) <_ +oo /\ +oo <_ ( vol* ` RR ) ) )
16 5 12 15 mpbir2an 
 |-  ( vol* ` RR ) = +oo