| 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 |
|
uniioombl.m |
|- ( ph -> M e. NN ) |
| 12 |
|
uniioombl.m2 |
|- ( ph -> ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C ) |
| 13 |
|
uniioombl.k |
|- K = U. ( ( (,) o. G ) " ( 1 ... M ) ) |
| 14 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
| 15 |
|
inss2 |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) |
| 16 |
|
rexpssxrxp |
|- ( RR X. RR ) C_ ( RR* X. RR* ) |
| 17 |
15 16
|
sstri |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) |
| 18 |
|
fss |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> G : NN --> ( RR* X. RR* ) ) |
| 19 |
7 17 18
|
sylancl |
|- ( ph -> G : NN --> ( RR* X. RR* ) ) |
| 20 |
|
fco |
|- ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ G : NN --> ( RR* X. RR* ) ) -> ( (,) o. G ) : NN --> ~P RR ) |
| 21 |
14 19 20
|
sylancr |
|- ( ph -> ( (,) o. G ) : NN --> ~P RR ) |
| 22 |
|
ffun |
|- ( ( (,) o. G ) : NN --> ~P RR -> Fun ( (,) o. G ) ) |
| 23 |
|
funiunfv |
|- ( Fun ( (,) o. G ) -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U. ( ( (,) o. G ) " ( 1 ... M ) ) ) |
| 24 |
21 22 23
|
3syl |
|- ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U. ( ( (,) o. G ) " ( 1 ... M ) ) ) |
| 25 |
|
elfznn |
|- ( j e. ( 1 ... M ) -> j e. NN ) |
| 26 |
|
fvco3 |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( ( (,) o. G ) ` j ) = ( (,) ` ( G ` j ) ) ) |
| 27 |
7 25 26
|
syl2an |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) o. G ) ` j ) = ( (,) ` ( G ` j ) ) ) |
| 28 |
27
|
iuneq2dv |
|- ( ph -> U_ j e. ( 1 ... M ) ( ( (,) o. G ) ` j ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) |
| 29 |
24 28
|
eqtr3d |
|- ( ph -> U. ( ( (,) o. G ) " ( 1 ... M ) ) = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) |
| 30 |
13 29
|
eqtrid |
|- ( ph -> K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) |
| 31 |
|
ffvelcdm |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) ) |
| 32 |
7 25 31
|
syl2an |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) ) |
| 33 |
32
|
elin2d |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( RR X. RR ) ) |
| 34 |
|
1st2nd2 |
|- ( ( G ` j ) e. ( RR X. RR ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) |
| 35 |
33 34
|
syl |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) |
| 36 |
35
|
fveq2d |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) ) |
| 37 |
|
df-ov |
|- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) |
| 38 |
36 37
|
eqtr4di |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) |
| 39 |
|
ioossre |
|- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) C_ RR |
| 40 |
38 39
|
eqsstrdi |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) C_ RR ) |
| 41 |
40
|
ralrimiva |
|- ( ph -> A. j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR ) |
| 42 |
|
iunss |
|- ( U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR <-> A. j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR ) |
| 43 |
41 42
|
sylibr |
|- ( ph -> U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR ) |
| 44 |
30 43
|
eqsstrd |
|- ( ph -> K C_ RR ) |
| 45 |
|
fzfid |
|- ( ph -> ( 1 ... M ) e. Fin ) |
| 46 |
38
|
fveq2d |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) ) |
| 47 |
|
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 ) ) ) ) |
| 48 |
7 25 47
|
syl2an |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) ) |
| 49 |
|
ovolioo |
|- ( ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) -> ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) ) |
| 50 |
48 49
|
syl |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) ) |
| 51 |
46 50
|
eqtrd |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) ) |
| 52 |
48
|
simp2d |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 2nd ` ( G ` j ) ) e. RR ) |
| 53 |
48
|
simp1d |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1st ` ( G ` j ) ) e. RR ) |
| 54 |
52 53
|
resubcld |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR ) |
| 55 |
51 54
|
eqeltrd |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) |
| 56 |
45 55
|
fsumrecl |
|- ( ph -> sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) |
| 57 |
30
|
fveq2d |
|- ( ph -> ( vol* ` K ) = ( vol* ` U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) ) |
| 58 |
40 55
|
jca |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( (,) ` ( G ` j ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) ) |
| 59 |
58
|
ralrimiva |
|- ( ph -> A. j e. ( 1 ... M ) ( ( (,) ` ( G ` j ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) ) |
| 60 |
|
ovolfiniun |
|- ( ( ( 1 ... M ) e. Fin /\ A. j e. ( 1 ... M ) ( ( (,) ` ( G ` j ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) ) -> ( vol* ` U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) <_ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) ) |
| 61 |
45 59 60
|
syl2anc |
|- ( ph -> ( vol* ` U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) <_ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) ) |
| 62 |
57 61
|
eqbrtrd |
|- ( ph -> ( vol* ` K ) <_ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) ) |
| 63 |
|
ovollecl |
|- ( ( K C_ RR /\ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR /\ ( vol* ` K ) <_ sum_ j e. ( 1 ... M ) ( vol* ` ( (,) ` ( G ` j ) ) ) ) -> ( vol* ` K ) e. RR ) |
| 64 |
44 56 62 63
|
syl3anc |
|- ( ph -> ( vol* ` K ) e. RR ) |
| 65 |
30 64
|
jca |
|- ( ph -> ( K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) /\ ( vol* ` K ) e. RR ) ) |