Metamath Proof Explorer

Theorem volicoff

Description: ( ( vol o. [,) ) o. F ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis volicoff.1 
|- ( ph -> F : A --> ( RR X. RR* ) )
Assertion volicoff 
|- ( ph -> ( ( vol o. [,) ) o. F ) : A --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 volicoff.1 
 |-  ( ph -> F : A --> ( RR X. RR* ) )
2 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
3 2 a1i 
 |-  ( ph -> vol : dom vol --> ( 0 [,] +oo ) )
4 icof 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
5 4 a1i 
 |-  ( ph -> [,) : ( RR* X. RR* ) --> ~P RR* )
6 ressxr 
 |-  RR C_ RR*
7 xpss1 
 |-  ( RR C_ RR* -> ( RR X. RR* ) C_ ( RR* X. RR* ) )
8 6 7 ax-mp 
 |-  ( RR X. RR* ) C_ ( RR* X. RR* )
9 8 a1i 
 |-  ( ph -> ( RR X. RR* ) C_ ( RR* X. RR* ) )
10 5 9 1 fcoss 
 |-  ( ph -> ( [,) o. F ) : A --> ~P RR* )
11 10 ffnd 
 |-  ( ph -> ( [,) o. F ) Fn A )
12 1 adantr 
 |-  ( ( ph /\ x e. A ) -> F : A --> ( RR X. RR* ) )
13 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
14 12 13 fvovco 
 |-  ( ( ph /\ x e. A ) -> ( ( [,) o. F ) ` x ) = ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) )
15 1 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. ( RR X. RR* ) )
16 xp1st 
 |-  ( ( F ` x ) e. ( RR X. RR* ) -> ( 1st ` ( F ` x ) ) e. RR )
17 15 16 syl 
 |-  ( ( ph /\ x e. A ) -> ( 1st ` ( F ` x ) ) e. RR )
18 xp2nd 
 |-  ( ( F ` x ) e. ( RR X. RR* ) -> ( 2nd ` ( F ` x ) ) e. RR* )
19 15 18 syl 
 |-  ( ( ph /\ x e. A ) -> ( 2nd ` ( F ` x ) ) e. RR* )
20 icombl 
 |-  ( ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR* ) -> ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) e. dom vol )
21 17 19 20 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) e. dom vol )
22 14 21 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> ( ( [,) o. F ) ` x ) e. dom vol )
23 22 ralrimiva 
 |-  ( ph -> A. x e. A ( ( [,) o. F ) ` x ) e. dom vol )
24 fnfvrnss 
 |-  ( ( ( [,) o. F ) Fn A /\ A. x e. A ( ( [,) o. F ) ` x ) e. dom vol ) -> ran ( [,) o. F ) C_ dom vol )
25 11 23 24 syl2anc 
 |-  ( ph -> ran ( [,) o. F ) C_ dom vol )
26 ffrn 
 |-  ( ( [,) o. F ) : A --> ~P RR* -> ( [,) o. F ) : A --> ran ( [,) o. F ) )
27 10 26 syl 
 |-  ( ph -> ( [,) o. F ) : A --> ran ( [,) o. F ) )
28 3 25 27 fcoss 
 |-  ( ph -> ( vol o. ( [,) o. F ) ) : A --> ( 0 [,] +oo ) )
29 coass 
 |-  ( ( vol o. [,) ) o. F ) = ( vol o. ( [,) o. F ) )
30 29 feq1i 
 |-  ( ( ( vol o. [,) ) o. F ) : A --> ( 0 [,] +oo ) <-> ( vol o. ( [,) o. F ) ) : A --> ( 0 [,] +oo ) )
31 30 a1i 
 |-  ( ph -> ( ( ( vol o. [,) ) o. F ) : A --> ( 0 [,] +oo ) <-> ( vol o. ( [,) o. F ) ) : A --> ( 0 [,] +oo ) ) )
32 28 31 mpbird 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) : A --> ( 0 [,] +oo ) )