Metamath Proof Explorer

Theorem ovnsubaddlem2

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnsubaddlem2.x 
|- ( ph -> X e. Fin )
ovnsubaddlem2.n0 
|- ( ph -> X =/= (/) )
ovnsubaddlem2.a 
|- ( ph -> A : NN --> ~P ( RR ^m X ) )
ovnsubaddlem2.e 
|- ( ph -> E e. RR+ )
ovnsubaddlem2.z 
|- Z = ( a e. ~P ( RR ^m X ) |-> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )
ovnsubaddlem2.c 
|- C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
ovnsubaddlem2.l 
|- L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
ovnsubaddlem2.d 
|- D = ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) )
Assertion ovnsubaddlem2 
|- ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )

Proof

Step Hyp Ref Expression
1 ovnsubaddlem2.x 
 |-  ( ph -> X e. Fin )
2 ovnsubaddlem2.n0 
 |-  ( ph -> X =/= (/) )
3 ovnsubaddlem2.a 
 |-  ( ph -> A : NN --> ~P ( RR ^m X ) )
4 ovnsubaddlem2.e 
 |-  ( ph -> E e. RR+ )
5 ovnsubaddlem2.z 
 |-  Z = ( a e. ~P ( RR ^m X ) |-> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )
6 ovnsubaddlem2.c 
 |-  C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
7 ovnsubaddlem2.l 
 |-  L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
8 ovnsubaddlem2.d 
 |-  D = ( a e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) )
9 fvex 
 |-  ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) e. _V
10 nnenom 
 |-  NN ~~ _om
11 9 10 axcc3 
 |-  E. g ( g Fn NN /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
12 simprl 
 |-  ( ( ph /\ ( g Fn NN /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) ) -> g Fn NN )
13 nfv 
 |-  F/ n ph
14 nfra1 
 |-  F/ n A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
15 13 14 nfan 
 |-  F/ n ( ph /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
16 rspa 
 |-  ( ( A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) /\ n e. NN ) -> ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
17 16 adantll 
 |-  ( ( ( ph /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) /\ n e. NN ) -> ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
18 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. Fin )
19 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> X =/= (/) )
20 3 adantr 
 |-  ( ( ph /\ n e. NN ) -> A : NN --> ~P ( RR ^m X ) )
21 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
22 20 21 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. ~P ( RR ^m X ) )
23 elpwi 
 |-  ( ( A ` n ) e. ~P ( RR ^m X ) -> ( A ` n ) C_ ( RR ^m X ) )
24 22 23 syl 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) C_ ( RR ^m X ) )
25 4 adantr 
 |-  ( ( ph /\ n e. NN ) -> E e. RR+ )
26 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
27 2nn 
 |-  2 e. NN
28 27 a1i 
 |-  ( n e. NN0 -> 2 e. NN )
29 id 
 |-  ( n e. NN0 -> n e. NN0 )
30 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
31 28 29 30 syl2anc 
 |-  ( n e. NN0 -> ( 2 ^ n ) e. NN )
32 nnrp 
 |-  ( ( 2 ^ n ) e. NN -> ( 2 ^ n ) e. RR+ )
33 31 32 syl 
 |-  ( n e. NN0 -> ( 2 ^ n ) e. RR+ )
34 26 33 syl 
 |-  ( n e. NN -> ( 2 ^ n ) e. RR+ )
35 34 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR+ )
36 25 35 rpdivcld 
 |-  ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. RR+ )
37 18 19 24 36 6 7 8 ovncvrrp 
 |-  ( ( ph /\ n e. NN ) -> E. i i e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
38 n0 
 |-  ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) <-> E. i i e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
39 37 38 sylibr 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) )
40 39 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) )
41 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
42 40 41 mpd 
 |-  ( ( ( ph /\ n e. NN ) /\ ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
43 42 ex 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
44 43 adantlr 
 |-  ( ( ( ph /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) /\ n e. NN ) -> ( ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
45 17 44 mpd 
 |-  ( ( ( ph /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) /\ n e. NN ) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
46 45 ex 
 |-  ( ( ph /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> ( n e. NN -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
47 15 46 ralrimi 
 |-  ( ( ph /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
48 47 adantrl 
 |-  ( ( ph /\ ( g Fn NN /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) ) -> A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
49 12 48 jca 
 |-  ( ( ph /\ ( g Fn NN /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) ) -> ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
50 49 ex 
 |-  ( ph -> ( ( g Fn NN /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) )
51 50 eximdv 
 |-  ( ph -> ( E. g ( g Fn NN /\ A. n e. NN ( ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) =/= (/) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> E. g ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) )
52 11 51 mpi 
 |-  ( ph -> E. g ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
53 simpl 
 |-  ( ( ph /\ ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> ph )
54 simprl 
 |-  ( ( ph /\ ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> g Fn NN )
55 simprr 
 |-  ( ( ph /\ ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
56 nnf1oxpnn 
 |-  E. f f : NN -1-1-onto-> ( NN X. NN )
57 simpl1 
 |-  ( ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> ph )
58 simpl2 
 |-  ( ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> g Fn NN )
59 fveq2 
 |-  ( q = n -> ( g ` q ) = ( g ` n ) )
60 2fveq3 
 |-  ( q = n -> ( D ` ( A ` q ) ) = ( D ` ( A ` n ) ) )
61 oveq2 
 |-  ( q = n -> ( 2 ^ q ) = ( 2 ^ n ) )
62 61 oveq2d 
 |-  ( q = n -> ( E / ( 2 ^ q ) ) = ( E / ( 2 ^ n ) ) )
63 60 62 fveq12d 
 |-  ( q = n -> ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) = ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
64 59 63 eleq12d 
 |-  ( q = n -> ( ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) <-> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) )
65 64 cbvralvw 
 |-  ( A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) <-> A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
66 65 biimpri 
 |-  ( A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) -> A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) )
67 66 3ad2ant3 
 |-  ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) -> A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) )
68 67 adantr 
 |-  ( ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) )
69 simpr 
 |-  ( ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> f : NN -1-1-onto-> ( NN X. NN ) )
70 1 adantr 
 |-  ( ( ph /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> X e. Fin )
71 70 3ad2antl1 
 |-  ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> X e. Fin )
72 2 adantr 
 |-  ( ( ph /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> X =/= (/) )
73 72 3ad2antl1 
 |-  ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> X =/= (/) )
74 3 adantr 
 |-  ( ( ph /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> A : NN --> ~P ( RR ^m X ) )
75 74 3ad2antl1 
 |-  ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> A : NN --> ~P ( RR ^m X ) )
76 4 adantr 
 |-  ( ( ph /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> E e. RR+ )
77 76 3ad2antl1 
 |-  ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> E e. RR+ )
78 coeq2 
 |-  ( h = i -> ( [,) o. h ) = ( [,) o. i ) )
79 78 fveq1d 
 |-  ( h = i -> ( ( [,) o. h ) ` k ) = ( ( [,) o. i ) ` k ) )
80 79 fveq2d 
 |-  ( h = i -> ( vol ` ( ( [,) o. h ) ` k ) ) = ( vol ` ( ( [,) o. i ) ` k ) ) )
81 80 prodeq2ad 
 |-  ( h = i -> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
82 81 cbvmptv 
 |-  ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
83 7 82 eqtri 
 |-  L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
84 65 biimpi 
 |-  ( A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) -> A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
85 84 3ad2ant3 
 |-  ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) -> A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
86 85 ad2antrr 
 |-  ( ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) /\ n e. NN ) -> A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
87 simpr 
 |-  ( ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) /\ n e. NN ) -> n e. NN )
88 rspa 
 |-  ( ( A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) /\ n e. NN ) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
89 86 87 88 syl2anc 
 |-  ( ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) /\ n e. NN ) -> ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
90 simpr 
 |-  ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> f : NN -1-1-onto-> ( NN X. NN ) )
91 2fveq3 
 |-  ( q = m -> ( 1st ` ( f ` q ) ) = ( 1st ` ( f ` m ) ) )
92 91 fveq2d 
 |-  ( q = m -> ( g ` ( 1st ` ( f ` q ) ) ) = ( g ` ( 1st ` ( f ` m ) ) ) )
93 2fveq3 
 |-  ( q = m -> ( 2nd ` ( f ` q ) ) = ( 2nd ` ( f ` m ) ) )
94 92 93 fveq12d 
 |-  ( q = m -> ( ( g ` ( 1st ` ( f ` q ) ) ) ` ( 2nd ` ( f ` q ) ) ) = ( ( g ` ( 1st ` ( f ` m ) ) ) ` ( 2nd ` ( f ` m ) ) ) )
95 94 cbvmptv 
 |-  ( q e. NN |-> ( ( g ` ( 1st ` ( f ` q ) ) ) ` ( 2nd ` ( f ` q ) ) ) ) = ( m e. NN |-> ( ( g ` ( 1st ` ( f ` m ) ) ) ` ( 2nd ` ( f ` m ) ) ) )
96 71 73 75 77 5 6 83 8 89 90 95 ovnsubaddlem1 
 |-  ( ( ( ph /\ g Fn NN /\ A. q e. NN ( g ` q ) e. ( ( D ` ( A ` q ) ) ` ( E / ( 2 ^ q ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )
97 57 58 68 69 96 syl31anc 
 |-  ( ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) /\ f : NN -1-1-onto-> ( NN X. NN ) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )
98 97 ex 
 |-  ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) -> ( f : NN -1-1-onto-> ( NN X. NN ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) ) )
99 98 exlimdv 
 |-  ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) -> ( E. f f : NN -1-1-onto-> ( NN X. NN ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) ) )
100 56 99 mpi 
 |-  ( ( ph /\ g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )
101 53 54 55 100 syl3anc 
 |-  ( ( ph /\ ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )
102 101 ex 
 |-  ( ph -> ( ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) ) )
103 102 exlimdv 
 |-  ( ph -> ( E. g ( g Fn NN /\ A. n e. NN ( g ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) ) )
104 52 103 mpd 
 |-  ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )