Metamath Proof Explorer

Theorem volf

Description: The domain and range of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Assertion volf 
|- vol : dom vol --> ( 0 [,] +oo )

Proof

Step Hyp Ref Expression
1 ovolf 
 |-  vol* : ~P RR --> ( 0 [,] +oo )
2 ffun 
 |-  ( vol* : ~P RR --> ( 0 [,] +oo ) -> Fun vol* )
3 funres 
 |-  ( Fun vol* -> Fun ( vol* |` dom vol ) )
4 1 2 3 mp2b 
 |-  Fun ( vol* |` dom vol )
5 volres 
 |-  vol = ( vol* |` dom vol )
6 5 funeqi 
 |-  ( Fun vol <-> Fun ( vol* |` dom vol ) )
7 4 6 mpbir 
 |-  Fun vol
8 resss 
 |-  ( vol* |` dom vol ) C_ vol*
9 5 8 eqsstri 
 |-  vol C_ vol*
10 fssxp 
 |-  ( vol* : ~P RR --> ( 0 [,] +oo ) -> vol* C_ ( ~P RR X. ( 0 [,] +oo ) ) )
11 1 10 ax-mp 
 |-  vol* C_ ( ~P RR X. ( 0 [,] +oo ) )
12 9 11 sstri 
 |-  vol C_ ( ~P RR X. ( 0 [,] +oo ) )
13 7 12 pm3.2i 
 |-  ( Fun vol /\ vol C_ ( ~P RR X. ( 0 [,] +oo ) ) )
14 funssxp 
 |-  ( ( Fun vol /\ vol C_ ( ~P RR X. ( 0 [,] +oo ) ) ) <-> ( vol : dom vol --> ( 0 [,] +oo ) /\ dom vol C_ ~P RR ) )
15 13 14 mpbi 
 |-  ( vol : dom vol --> ( 0 [,] +oo ) /\ dom vol C_ ~P RR )
16 15 simpli 
 |-  vol : dom vol --> ( 0 [,] +oo )