Metamath Proof Explorer

Theorem volioof

Description: The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion volioof 
|- ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo )

Proof

Step Hyp Ref Expression
1 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
2 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
3 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
4 2 3 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
5 df-ov 
 |-  ( ( 1st ` x ) (,) ( 2nd ` x ) ) = ( (,) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
6 5 a1i 
 |-  ( x e. ( RR* X. RR* ) -> ( ( 1st ` x ) (,) ( 2nd ` x ) ) = ( (,) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
7 1st2nd2 
 |-  ( x e. ( RR* X. RR* ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
8 7 eqcomd 
 |-  ( x e. ( RR* X. RR* ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = x )
9 8 fveq2d 
 |-  ( x e. ( RR* X. RR* ) -> ( (,) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) = ( (,) ` x ) )
10 6 9 eqtr2d 
 |-  ( x e. ( RR* X. RR* ) -> ( (,) ` x ) = ( ( 1st ` x ) (,) ( 2nd ` x ) ) )
11 ioombl 
 |-  ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol
12 10 11 eqeltrdi 
 |-  ( x e. ( RR* X. RR* ) -> ( (,) ` x ) e. dom vol )
13 12 rgen 
 |-  A. x e. ( RR* X. RR* ) ( (,) ` x ) e. dom vol
14 4 13 pm3.2i 
 |-  ( (,) Fn ( RR* X. RR* ) /\ A. x e. ( RR* X. RR* ) ( (,) ` x ) e. dom vol )
15 ffnfv 
 |-  ( (,) : ( RR* X. RR* ) --> dom vol <-> ( (,) Fn ( RR* X. RR* ) /\ A. x e. ( RR* X. RR* ) ( (,) ` x ) e. dom vol ) )
16 14 15 mpbir 
 |-  (,) : ( RR* X. RR* ) --> dom vol
17 fco 
 |-  ( ( vol : dom vol --> ( 0 [,] +oo ) /\ (,) : ( RR* X. RR* ) --> dom vol ) -> ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo ) )
18 1 16 17 mp2an 
 |-  ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo )