| Step |
Hyp |
Ref |
Expression |
| 1 |
|
uniioombl.1 |
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
| 2 |
|
uniioombl.2 |
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) ) |
| 3 |
|
uniioombl.3 |
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) ) |
| 4 |
|
uniioombl.a |
|- A = U. ran ( (,) o. F ) |
| 5 |
|
uniioombl.e |
|- ( ph -> ( vol* ` E ) e. RR ) |
| 6 |
|
uniioombl.c |
|- ( ph -> C e. RR+ ) |
| 7 |
|
uniioombl.g |
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
| 8 |
|
uniioombl.s |
|- ( ph -> E C_ U. ran ( (,) o. G ) ) |
| 9 |
|
uniioombl.t |
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) ) |
| 10 |
|
uniioombl.v |
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) ) |
| 11 |
|
eqid |
|- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G ) |
| 12 |
11 9
|
ovolsf |
|- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) ) |
| 13 |
7 12
|
syl |
|- ( ph -> T : NN --> ( 0 [,) +oo ) ) |
| 14 |
13
|
frnd |
|- ( ph -> ran T C_ ( 0 [,) +oo ) ) |
| 15 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
| 16 |
14 15
|
sstrdi |
|- ( ph -> ran T C_ RR ) |
| 17 |
|
1nn |
|- 1 e. NN |
| 18 |
13
|
fdmd |
|- ( ph -> dom T = NN ) |
| 19 |
17 18
|
eleqtrrid |
|- ( ph -> 1 e. dom T ) |
| 20 |
19
|
ne0d |
|- ( ph -> dom T =/= (/) ) |
| 21 |
|
dm0rn0 |
|- ( dom T = (/) <-> ran T = (/) ) |
| 22 |
21
|
necon3bii |
|- ( dom T =/= (/) <-> ran T =/= (/) ) |
| 23 |
20 22
|
sylib |
|- ( ph -> ran T =/= (/) ) |
| 24 |
|
icossxr |
|- ( 0 [,) +oo ) C_ RR* |
| 25 |
14 24
|
sstrdi |
|- ( ph -> ran T C_ RR* ) |
| 26 |
|
supxrcl |
|- ( ran T C_ RR* -> sup ( ran T , RR* , < ) e. RR* ) |
| 27 |
25 26
|
syl |
|- ( ph -> sup ( ran T , RR* , < ) e. RR* ) |
| 28 |
6
|
rpred |
|- ( ph -> C e. RR ) |
| 29 |
5 28
|
readdcld |
|- ( ph -> ( ( vol* ` E ) + C ) e. RR ) |
| 30 |
29
|
rexrd |
|- ( ph -> ( ( vol* ` E ) + C ) e. RR* ) |
| 31 |
|
pnfxr |
|- +oo e. RR* |
| 32 |
31
|
a1i |
|- ( ph -> +oo e. RR* ) |
| 33 |
29
|
ltpnfd |
|- ( ph -> ( ( vol* ` E ) + C ) < +oo ) |
| 34 |
27 30 32 10 33
|
xrlelttrd |
|- ( ph -> sup ( ran T , RR* , < ) < +oo ) |
| 35 |
|
supxrbnd |
|- ( ( ran T C_ RR /\ ran T =/= (/) /\ sup ( ran T , RR* , < ) < +oo ) -> sup ( ran T , RR* , < ) e. RR ) |
| 36 |
16 23 34 35
|
syl3anc |
|- ( ph -> sup ( ran T , RR* , < ) e. RR ) |