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 |
|
ffvelrn |
|- ( ( 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 ) ) |