| 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 |
1
|
adantr |
|- ( ( ph /\ J e. NN ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
| 12 |
11
|
ffvelcdmda |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( F ` z ) e. ( <_ i^i ( RR X. RR ) ) ) |
| 13 |
12
|
elin2d |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( F ` z ) e. ( RR X. RR ) ) |
| 14 |
|
1st2nd2 |
|- ( ( F ` z ) e. ( RR X. RR ) -> ( F ` z ) = <. ( 1st ` ( F ` z ) ) , ( 2nd ` ( F ` z ) ) >. ) |
| 15 |
13 14
|
syl |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( F ` z ) = <. ( 1st ` ( F ` z ) ) , ( 2nd ` ( F ` z ) ) >. ) |
| 16 |
15
|
fveq2d |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( F ` z ) ) = ( (,) ` <. ( 1st ` ( F ` z ) ) , ( 2nd ` ( F ` z ) ) >. ) ) |
| 17 |
|
df-ov |
|- ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) = ( (,) ` <. ( 1st ` ( F ` z ) ) , ( 2nd ` ( F ` z ) ) >. ) |
| 18 |
16 17
|
eqtr4di |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( F ` z ) ) = ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) ) |
| 19 |
7
|
ffvelcdmda |
|- ( ( ph /\ J e. NN ) -> ( G ` J ) e. ( <_ i^i ( RR X. RR ) ) ) |
| 20 |
19
|
elin2d |
|- ( ( ph /\ J e. NN ) -> ( G ` J ) e. ( RR X. RR ) ) |
| 21 |
|
1st2nd2 |
|- ( ( G ` J ) e. ( RR X. RR ) -> ( G ` J ) = <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) |
| 22 |
20 21
|
syl |
|- ( ( ph /\ J e. NN ) -> ( G ` J ) = <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) |
| 23 |
22
|
fveq2d |
|- ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) = ( (,) ` <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) ) |
| 24 |
|
df-ov |
|- ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) = ( (,) ` <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) |
| 25 |
23 24
|
eqtr4di |
|- ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) = ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) |
| 26 |
25
|
adantr |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( G ` J ) ) = ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) |
| 27 |
18 26
|
ineq12d |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) = ( ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) i^i ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) ) |
| 28 |
|
ovolfcl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ z e. NN ) -> ( ( 1st ` ( F ` z ) ) e. RR /\ ( 2nd ` ( F ` z ) ) e. RR /\ ( 1st ` ( F ` z ) ) <_ ( 2nd ` ( F ` z ) ) ) ) |
| 29 |
11 28
|
sylan |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( 1st ` ( F ` z ) ) e. RR /\ ( 2nd ` ( F ` z ) ) e. RR /\ ( 1st ` ( F ` z ) ) <_ ( 2nd ` ( F ` z ) ) ) ) |
| 30 |
29
|
simp1d |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 1st ` ( F ` z ) ) e. RR ) |
| 31 |
30
|
rexrd |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 1st ` ( F ` z ) ) e. RR* ) |
| 32 |
29
|
simp2d |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 2nd ` ( F ` z ) ) e. RR ) |
| 33 |
32
|
rexrd |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 2nd ` ( F ` z ) ) e. RR* ) |
| 34 |
|
ovolfcl |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ J e. NN ) -> ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) ) |
| 35 |
7 34
|
sylan |
|- ( ( ph /\ J e. NN ) -> ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) ) |
| 36 |
35
|
simp1d |
|- ( ( ph /\ J e. NN ) -> ( 1st ` ( G ` J ) ) e. RR ) |
| 37 |
36
|
rexrd |
|- ( ( ph /\ J e. NN ) -> ( 1st ` ( G ` J ) ) e. RR* ) |
| 38 |
37
|
adantr |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 1st ` ( G ` J ) ) e. RR* ) |
| 39 |
35
|
simp2d |
|- ( ( ph /\ J e. NN ) -> ( 2nd ` ( G ` J ) ) e. RR ) |
| 40 |
39
|
rexrd |
|- ( ( ph /\ J e. NN ) -> ( 2nd ` ( G ` J ) ) e. RR* ) |
| 41 |
40
|
adantr |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 2nd ` ( G ` J ) ) e. RR* ) |
| 42 |
|
iooin |
|- ( ( ( ( 1st ` ( F ` z ) ) e. RR* /\ ( 2nd ` ( F ` z ) ) e. RR* ) /\ ( ( 1st ` ( G ` J ) ) e. RR* /\ ( 2nd ` ( G ` J ) ) e. RR* ) ) -> ( ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) i^i ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) = ( if ( ( 1st ` ( F ` z ) ) <_ ( 1st ` ( G ` J ) ) , ( 1st ` ( G ` J ) ) , ( 1st ` ( F ` z ) ) ) (,) if ( ( 2nd ` ( F ` z ) ) <_ ( 2nd ` ( G ` J ) ) , ( 2nd ` ( F ` z ) ) , ( 2nd ` ( G ` J ) ) ) ) ) |
| 43 |
31 33 38 41 42
|
syl22anc |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) i^i ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) = ( if ( ( 1st ` ( F ` z ) ) <_ ( 1st ` ( G ` J ) ) , ( 1st ` ( G ` J ) ) , ( 1st ` ( F ` z ) ) ) (,) if ( ( 2nd ` ( F ` z ) ) <_ ( 2nd ` ( G ` J ) ) , ( 2nd ` ( F ` z ) ) , ( 2nd ` ( G ` J ) ) ) ) ) |
| 44 |
27 43
|
eqtrd |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) = ( if ( ( 1st ` ( F ` z ) ) <_ ( 1st ` ( G ` J ) ) , ( 1st ` ( G ` J ) ) , ( 1st ` ( F ` z ) ) ) (,) if ( ( 2nd ` ( F ` z ) ) <_ ( 2nd ` ( G ` J ) ) , ( 2nd ` ( F ` z ) ) , ( 2nd ` ( G ` J ) ) ) ) ) |
| 45 |
|
ioorebas |
|- ( if ( ( 1st ` ( F ` z ) ) <_ ( 1st ` ( G ` J ) ) , ( 1st ` ( G ` J ) ) , ( 1st ` ( F ` z ) ) ) (,) if ( ( 2nd ` ( F ` z ) ) <_ ( 2nd ` ( G ` J ) ) , ( 2nd ` ( F ` z ) ) , ( 2nd ` ( G ` J ) ) ) ) e. ran (,) |
| 46 |
44 45
|
eqeltrdi |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) ) |