Step |
Hyp |
Ref |
Expression |
1 |
|
pnfnre |
|- +oo e/ RR |
2 |
1
|
neli |
|- -. +oo e. RR |
3 |
|
rembl |
|- RR e. dom vol |
4 |
|
mblvol |
|- ( RR e. dom vol -> ( vol ` RR ) = ( vol* ` RR ) ) |
5 |
3 4
|
ax-mp |
|- ( vol ` RR ) = ( vol* ` RR ) |
6 |
|
ovolre |
|- ( vol* ` RR ) = +oo |
7 |
5 6
|
eqtri |
|- ( vol ` RR ) = +oo |
8 |
|
cnvimarndm |
|- ( `' F " ran F ) = dom F |
9 |
|
i1ff |
|- ( F e. dom S.1 -> F : RR --> RR ) |
10 |
9
|
fdmd |
|- ( F e. dom S.1 -> dom F = RR ) |
11 |
10
|
adantr |
|- ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> dom F = RR ) |
12 |
8 11
|
syl5eq |
|- ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> ( `' F " ran F ) = RR ) |
13 |
12
|
fveq2d |
|- ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> ( vol ` ( `' F " ran F ) ) = ( vol ` RR ) ) |
14 |
|
i1fima2 |
|- ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> ( vol ` ( `' F " ran F ) ) e. RR ) |
15 |
13 14
|
eqeltrrd |
|- ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> ( vol ` RR ) e. RR ) |
16 |
7 15
|
eqeltrrid |
|- ( ( F e. dom S.1 /\ -. 0 e. ran F ) -> +oo e. RR ) |
17 |
16
|
ex |
|- ( F e. dom S.1 -> ( -. 0 e. ran F -> +oo e. RR ) ) |
18 |
2 17
|
mt3i |
|- ( F e. dom S.1 -> 0 e. ran F ) |