Metamath Proof Explorer

Theorem uniioombllem6

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.2 
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
uniioombl.3 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
uniioombl.a 
|- A = U. ran ( (,) o. F )
uniioombl.e 
|- ( ph -> ( vol* ` E ) e. RR )
uniioombl.c 
|- ( ph -> C e. RR+ )
uniioombl.g 
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.s 
|- ( ph -> E C_ U. ran ( (,) o. G ) )
uniioombl.t 
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
uniioombl.v 
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
Assertion uniioombllem6 
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )

Proof

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 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 1zzd 
 |-  ( ph -> 1 e. ZZ )
13 eqidd 
 |-  ( ( ph /\ m e. NN ) -> ( T ` m ) = ( T ` m ) )
14 eqidd 
 |-  ( ( ph /\ a e. NN ) -> ( ( ( abs o. - ) o. G ) ` a ) = ( ( ( abs o. - ) o. G ) ` a ) )
15 eqid 
 |-  ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
16 15 ovolfsf 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
17 7 16 syl 
 |-  ( ph -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
18 17 ffvelcdmda 
 |-  ( ( ph /\ a e. NN ) -> ( ( ( abs o. - ) o. G ) ` a ) e. ( 0 [,) +oo ) )
19 elrege0 
 |-  ( ( ( ( abs o. - ) o. G ) ` a ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. G ) ` a ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` a ) ) )
20 18 19 sylib 
 |-  ( ( ph /\ a e. NN ) -> ( ( ( ( abs o. - ) o. G ) ` a ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. G ) ` a ) ) )
21 20 simpld 
 |-  ( ( ph /\ a e. NN ) -> ( ( ( abs o. - ) o. G ) ` a ) e. RR )
22 20 simprd 
 |-  ( ( ph /\ a e. NN ) -> 0 <_ ( ( ( abs o. - ) o. G ) ` a ) )
23 1 2 3 4 5 6 7 8 9 10 uniioombllem1 
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR )
24 15 9 ovolsf 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) )
25 7 24 syl 
 |-  ( ph -> T : NN --> ( 0 [,) +oo ) )
26 25 frnd 
 |-  ( ph -> ran T C_ ( 0 [,) +oo ) )
27 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
28 26 27 sstrdi 
 |-  ( ph -> ran T C_ RR* )
29 supxrub 
 |-  ( ( ran T C_ RR* /\ x e. ran T ) -> x <_ sup ( ran T , RR* , < ) )
30 28 29 sylan 
 |-  ( ( ph /\ x e. ran T ) -> x <_ sup ( ran T , RR* , < ) )
31 30 ralrimiva 
 |-  ( ph -> A. x e. ran T x <_ sup ( ran T , RR* , < ) )
32 25 ffnd 
 |-  ( ph -> T Fn NN )
33 breq1 
 |-  ( x = ( T ` m ) -> ( x <_ sup ( ran T , RR* , < ) <-> ( T ` m ) <_ sup ( ran T , RR* , < ) ) )
34 33 ralrn 
 |-  ( T Fn NN -> ( A. x e. ran T x <_ sup ( ran T , RR* , < ) <-> A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) ) )
35 32 34 syl 
 |-  ( ph -> ( A. x e. ran T x <_ sup ( ran T , RR* , < ) <-> A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) ) )
36 31 35 mpbid 
 |-  ( ph -> A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) )
37 brralrspcev 
 |-  ( ( sup ( ran T , RR* , < ) e. RR /\ A. m e. NN ( T ` m ) <_ sup ( ran T , RR* , < ) ) -> E. x e. RR A. m e. NN ( T ` m ) <_ x )
38 23 36 37 syl2anc 
 |-  ( ph -> E. x e. RR A. m e. NN ( T ` m ) <_ x )
39 11 9 12 14 21 22 38 isumsup2 
 |-  ( ph -> T ~~> sup ( ran T , RR , < ) )
40 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
41 26 40 sstrdi 
 |-  ( ph -> ran T C_ RR )
42 1nn 
 |-  1 e. NN
43 25 fdmd 
 |-  ( ph -> dom T = NN )
44 42 43 eleqtrrid 
 |-  ( ph -> 1 e. dom T )
45 44 ne0d 
 |-  ( ph -> dom T =/= (/) )
46 dm0rn0 
 |-  ( dom T = (/) <-> ran T = (/) )
47 46 necon3bii 
 |-  ( dom T =/= (/) <-> ran T =/= (/) )
48 45 47 sylib 
 |-  ( ph -> ran T =/= (/) )
49 brralrspcev 
 |-  ( ( sup ( ran T , RR* , < ) e. RR /\ A. x e. ran T x <_ sup ( ran T , RR* , < ) ) -> E. y e. RR A. x e. ran T x <_ y )
50 23 31 49 syl2anc 
 |-  ( ph -> E. y e. RR A. x e. ran T x <_ y )
51 supxrre 
 |-  ( ( ran T C_ RR /\ ran T =/= (/) /\ E. y e. RR A. x e. ran T x <_ y ) -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
52 41 48 50 51 syl3anc 
 |-  ( ph -> sup ( ran T , RR* , < ) = sup ( ran T , RR , < ) )
53 39 52 breqtrrd 
 |-  ( ph -> T ~~> sup ( ran T , RR* , < ) )
54 11 12 6 13 53 climi2 
 |-  ( ph -> E. j e. NN A. m e. ( ZZ>= ` j ) ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C )
55 11 r19.2uz 
 |-  ( E. j e. NN A. m e. ( ZZ>= ` j ) ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C -> E. m e. NN ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C )
56 54 55 syl 
 |-  ( ph -> E. m e. NN ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C )
57 1zzd 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> 1 e. ZZ )
58 6 ad2antrr 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> C e. RR+ )
59 simplrl 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> m e. NN )
60 59 nnrpd 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> m e. RR+ )
61 58 60 rpdivcld 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( C / m ) e. RR+ )
62 fvex 
 |-  ( (,) ` ( F ` z ) ) e. _V
63 62 inex1 
 |-  ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) e. _V
64 63 rgenw 
 |-  A. z e. NN ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) e. _V
65 eqid 
 |-  ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) )
66 65 fnmpt 
 |-  ( A. z e. NN ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) e. _V -> ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) Fn NN )
67 64 66 mp1i 
 |-  ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) Fn NN )
68 elfznn 
 |-  ( i e. ( 1 ... n ) -> i e. NN )
69 fvco2 
 |-  ( ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) Fn NN /\ i e. NN ) -> ( ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ` i ) = ( vol* ` ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) ) )
70 67 68 69 syl2an 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ` i ) = ( vol* ` ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) ) )
71 68 adantl 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> i e. NN )
72 2fveq3 
 |-  ( z = i -> ( (,) ` ( F ` z ) ) = ( (,) ` ( F ` i ) ) )
73 72 ineq1d 
 |-  ( z = i -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
74 fvex 
 |-  ( (,) ` ( F ` i ) ) e. _V
75 74 inex1 
 |-  ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) e. _V
76 73 65 75 fvmpt 
 |-  ( i e. NN -> ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) = ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
77 71 76 syl 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) = ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) )
78 77 fveq2d 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( vol* ` ( ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ` i ) ) = ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
79 70 78 eqtrd 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ` i ) = ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
80 simpr 
 |-  ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> n e. NN )
81 80 11 eleqtrdi 
 |-  ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
82 inss2 
 |-  ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( G ` j ) )
83 7 adantr 
 |-  ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
84 elfznn 
 |-  ( j e. ( 1 ... m ) -> j e. NN )
85 ffvelcdm 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
86 83 84 85 syl2an 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) )
87 86 elin2d 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( G ` j ) e. ( RR X. RR ) )
88 1st2nd2 
 |-  ( ( G ` j ) e. ( RR X. RR ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
89 87 88 syl 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
90 89 fveq2d 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( (,) ` ( G ` j ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) )
91 df-ov 
 |-  ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. )
92 90 91 eqtr4di 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( (,) ` ( G ` j ) ) = ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) )
93 ioossre 
 |-  ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) C_ RR
94 92 93 eqsstrdi 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
95 94 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( (,) ` ( G ` j ) ) C_ RR )
96 92 fveq2d 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) )
97 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 ) ) ) )
98 83 84 97 syl2an 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) )
99 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 ) ) ) )
100 98 99 syl 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( vol* ` ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
101 96 100 eqtrd 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) )
102 98 simp2d 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( 2nd ` ( G ` j ) ) e. RR )
103 98 simp1d 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( 1st ` ( G ` j ) ) e. RR )
104 102 103 resubcld 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR )
105 101 104 eqeltrd 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR )
106 105 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR )
107 ovolsscl 
 |-  ( ( ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) C_ ( (,) ` ( G ` j ) ) /\ ( (,) ` ( G ` j ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` j ) ) ) e. RR ) -> ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
108 82 95 106 107 mp3an2i 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. RR )
109 108 recnd 
 |-  ( ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) /\ i e. ( 1 ... n ) ) -> ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) e. CC )
110 79 81 109 fsumser 
 |-  ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ` n ) )
111 110 eqcomd 
 |-  ( ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) /\ n e. NN ) -> ( seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ` n ) = sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
112 2fveq3 
 |-  ( z = k -> ( (,) ` ( F ` z ) ) = ( (,) ` ( F ` k ) ) )
113 112 ineq1d 
 |-  ( z = k -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( F ` k ) ) i^i ( (,) ` ( G ` j ) ) ) )
114 113 cbvmptv 
 |-  ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( k e. NN |-> ( ( (,) ` ( F ` k ) ) i^i ( (,) ` ( G ` j ) ) ) )
115 eqeq1 
 |-  ( z = x -> ( z = (/) <-> x = (/) ) )
116 infeq1 
 |-  ( z = x -> inf ( z , RR* , < ) = inf ( x , RR* , < ) )
117 supeq1 
 |-  ( z = x -> sup ( z , RR* , < ) = sup ( x , RR* , < ) )
118 116 117 opeq12d 
 |-  ( z = x -> <. inf ( z , RR* , < ) , sup ( z , RR* , < ) >. = <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. )
119 115 118 ifbieq2d 
 |-  ( z = x -> if ( z = (/) , <. 0 , 0 >. , <. inf ( z , RR* , < ) , sup ( z , RR* , < ) >. ) = if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) )
120 119 cbvmptv 
 |-  ( z e. ran (,) |-> if ( z = (/) , <. 0 , 0 >. , <. inf ( z , RR* , < ) , sup ( z , RR* , < ) >. ) ) = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) )
121 1 2 3 4 5 6 7 8 9 10 114 120 uniioombllem2 
 |-  ( ( ph /\ j e. NN ) -> seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ~~> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) )
122 84 121 sylan2 
 |-  ( ( ph /\ j e. ( 1 ... m ) ) -> seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ~~> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) )
123 122 adantlr 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> seq 1 ( + , ( vol* o. ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) ) ) ~~> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) )
124 11 57 61 111 123 climi2 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> E. a e. NN A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
125 1z 
 |-  1 e. ZZ
126 11 rexuz3 
 |-  ( 1 e. ZZ -> ( E. a e. NN A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) )
127 125 126 ax-mp 
 |-  ( E. a e. NN A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
128 124 127 sylib 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ j e. ( 1 ... m ) ) -> E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
129 128 ralrimiva 
 |-  ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> A. j e. ( 1 ... m ) E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
130 fzfi 
 |-  ( 1 ... m ) e. Fin
131 rexfiuz 
 |-  ( ( 1 ... m ) e. Fin -> ( E. a e. ZZ A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> A. j e. ( 1 ... m ) E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) )
132 130 131 ax-mp 
 |-  ( E. a e. ZZ A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> A. j e. ( 1 ... m ) E. a e. ZZ A. n e. ( ZZ>= ` a ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
133 129 132 sylibr 
 |-  ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> E. a e. ZZ A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
134 11 rexuz3 
 |-  ( 1 e. ZZ -> ( E. a e. NN A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> E. a e. ZZ A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) )
135 125 134 ax-mp 
 |-  ( E. a e. NN A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> E. a e. ZZ A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
136 133 135 sylibr 
 |-  ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> E. a e. NN A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
137 11 r19.2uz 
 |-  ( E. a e. NN A. n e. ( ZZ>= ` a ) A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) -> E. n e. NN A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
138 136 137 syl 
 |-  ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> E. n e. NN A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
139 1 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
140 2 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
141 5 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> ( vol* ` E ) e. RR )
142 6 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> C e. RR+ )
143 7 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
144 8 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> E C_ U. ran ( (,) o. G ) )
145 10 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
146 simprll 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> m e. NN )
147 simprlr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C )
148 eqid 
 |-  U. ( ( (,) o. G ) " ( 1 ... m ) ) = U. ( ( (,) o. G ) " ( 1 ... m ) )
149 simprrl 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> n e. NN )
150 simprrr 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) )
151 2fveq3 
 |-  ( i = z -> ( (,) ` ( F ` i ) ) = ( (,) ` ( F ` z ) ) )
152 151 ineq1d 
 |-  ( i = z -> ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) )
153 152 fveq2d 
 |-  ( i = z -> ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) )
154 153 cbvsumv 
 |-  sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) )
155 2fveq3 
 |-  ( j = k -> ( (,) ` ( G ` j ) ) = ( (,) ` ( G ` k ) ) )
156 155 ineq2d 
 |-  ( j = k -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) )
157 156 fveq2d 
 |-  ( j = k -> ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) = ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) )
158 157 sumeq2sdv 
 |-  ( j = k -> sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) )
159 154 158 eqtrid 
 |-  ( j = k -> sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) = sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) )
160 155 ineq1d 
 |-  ( j = k -> ( ( (,) ` ( G ` j ) ) i^i A ) = ( ( (,) ` ( G ` k ) ) i^i A ) )
161 160 fveq2d 
 |-  ( j = k -> ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) = ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) )
162 159 161 oveq12d 
 |-  ( j = k -> ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) = ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) )
163 162 fveq2d 
 |-  ( j = k -> ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) = ( abs ` ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) ) )
164 163 breq1d 
 |-  ( j = k -> ( ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> ( abs ` ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) ) < ( C / m ) ) )
165 164 cbvralvw 
 |-  ( A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) <-> A. k e. ( 1 ... m ) ( abs ` ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) ) < ( C / m ) )
166 150 165 sylib 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> A. k e. ( 1 ... m ) ( abs ` ( sum_ z e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` k ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` k ) ) i^i A ) ) ) ) < ( C / m ) )
167 eqid 
 |-  U. ( ( (,) o. F ) " ( 1 ... n ) ) = U. ( ( (,) o. F ) " ( 1 ... n ) )
168 139 140 3 4 141 142 143 144 9 145 146 147 148 149 166 167 uniioombllem5 
 |-  ( ( ph /\ ( ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) ) -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
169 168 anassrs 
 |-  ( ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) /\ ( n e. NN /\ A. j e. ( 1 ... m ) ( abs ` ( sum_ i e. ( 1 ... n ) ( vol* ` ( ( (,) ` ( F ` i ) ) i^i ( (,) ` ( G ` j ) ) ) ) - ( vol* ` ( ( (,) ` ( G ` j ) ) i^i A ) ) ) ) < ( C / m ) ) ) -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
170 138 169 rexlimddv 
 |-  ( ( ph /\ ( m e. NN /\ ( abs ` ( ( T ` m ) - sup ( ran T , RR* , < ) ) ) < C ) ) -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )
171 56 170 rexlimddv 
 |-  ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) <_ ( ( vol* ` E ) + ( 4 x. C ) ) )