Metamath Proof Explorer

Theorem ovolf

Description: The domain and codomain of the outer volume function. (Contributed by Mario Carneiro, 16-Mar-2014) (Proof shortened by AV, 17-Sep-2020)

Ref Expression
Assertion ovolf 
|- vol* : ~P RR --> ( 0 [,] +oo )

Proof

Step Hyp Ref Expression
1 xrltso 
 |-  < Or RR*
2 1 infex 
 |-  inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) e. _V
3 df-ovol 
 |-  vol* = ( x e. ~P RR |-> inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
4 2 3 fnmpti 
 |-  vol* Fn ~P RR
5 elpwi 
 |-  ( x e. ~P RR -> x C_ RR )
6 ovolcl 
 |-  ( x C_ RR -> ( vol* ` x ) e. RR* )
7 ovolge0 
 |-  ( x C_ RR -> 0 <_ ( vol* ` x ) )
8 pnfge 
 |-  ( ( vol* ` x ) e. RR* -> ( vol* ` x ) <_ +oo )
9 6 8 syl 
 |-  ( x C_ RR -> ( vol* ` x ) <_ +oo )
10 0xr 
 |-  0 e. RR*
11 pnfxr 
 |-  +oo e. RR*
12 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( ( vol* ` x ) e. ( 0 [,] +oo ) <-> ( ( vol* ` x ) e. RR* /\ 0 <_ ( vol* ` x ) /\ ( vol* ` x ) <_ +oo ) ) )
13 10 11 12 mp2an 
 |-  ( ( vol* ` x ) e. ( 0 [,] +oo ) <-> ( ( vol* ` x ) e. RR* /\ 0 <_ ( vol* ` x ) /\ ( vol* ` x ) <_ +oo ) )
14 6 7 9 13 syl3anbrc 
 |-  ( x C_ RR -> ( vol* ` x ) e. ( 0 [,] +oo ) )
15 5 14 syl 
 |-  ( x e. ~P RR -> ( vol* ` x ) e. ( 0 [,] +oo ) )
16 15 rgen 
 |-  A. x e. ~P RR ( vol* ` x ) e. ( 0 [,] +oo )
17 ffnfv 
 |-  ( vol* : ~P RR --> ( 0 [,] +oo ) <-> ( vol* Fn ~P RR /\ A. x e. ~P RR ( vol* ` x ) e. ( 0 [,] +oo ) ) )
18 4 16 17 mpbir2an 
 |-  vol* : ~P RR --> ( 0 [,] +oo )