Metamath Proof Explorer

Theorem ovnsubaddlem1

Description: The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnsubaddlem1.x 
|- ( ph -> X e. Fin )
ovnsubaddlem1.n0 
|- ( ph -> X =/= (/) )
ovnsubaddlem1.a 
|- ( ph -> A : NN --> ~P ( RR ^m X ) )
ovnsubaddlem1.e 
|- ( ph -> E e. RR+ )
ovnsubaddlem1.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 ) ) ) ) ) } )
ovnsubaddlem1.c 
|- C = ( a e. ~P ( RR ^m X ) |-> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )
ovnsubaddlem1.l 
|- L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
ovnsubaddlem1.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 ) } ) )
ovnsubaddlem1.i 
|- ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
ovnsubaddlem1.f 
|- ( ph -> F : NN -1-1-onto-> ( NN X. NN ) )
ovnsubaddlem1.g 
|- G = ( m e. NN |-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )
Assertion ovnsubaddlem1 
|- ( 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 ovnsubaddlem1.x 
 |-  ( ph -> X e. Fin )
2 ovnsubaddlem1.n0 
 |-  ( ph -> X =/= (/) )
3 ovnsubaddlem1.a 
 |-  ( ph -> A : NN --> ~P ( RR ^m X ) )
4 ovnsubaddlem1.e 
 |-  ( ph -> E e. RR+ )
5 ovnsubaddlem1.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 ovnsubaddlem1.c 
 |-  C = ( a e. ~P ( RR ^m X ) |-> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )
7 ovnsubaddlem1.l 
 |-  L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
8 ovnsubaddlem1.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 ovnsubaddlem1.i 
 |-  ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) )
10 ovnsubaddlem1.f 
 |-  ( ph -> F : NN -1-1-onto-> ( NN X. NN ) )
11 ovnsubaddlem1.g 
 |-  G = ( m e. NN |-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )
12 3 adantr 
 |-  ( ( ph /\ n e. NN ) -> A : NN --> ~P ( RR ^m X ) )
13 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
14 12 13 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. ~P ( RR ^m X ) )
15 elpwi 
 |-  ( ( A ` n ) e. ~P ( RR ^m X ) -> ( A ` n ) C_ ( RR ^m X ) )
16 14 15 syl 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) C_ ( RR ^m X ) )
17 16 ralrimiva 
 |-  ( ph -> A. n e. NN ( A ` n ) C_ ( RR ^m X ) )
18 iunss 
 |-  ( U_ n e. NN ( A ` n ) C_ ( RR ^m X ) <-> A. n e. NN ( A ` n ) C_ ( RR ^m X ) )
19 17 18 sylibr 
 |-  ( ph -> U_ n e. NN ( A ` n ) C_ ( RR ^m X ) )
20 1 19 ovnxrcl 
 |-  ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) e. RR* )
21 nfv 
 |-  F/ m ph
22 nnex 
 |-  NN e. _V
23 22 a1i 
 |-  ( ph -> NN e. _V )
24 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
25 nfv 
 |-  F/ k ( ph /\ m e. NN )
26 simpl 
 |-  ( ( ph /\ m e. NN ) -> ph )
27 26 1 syl 
 |-  ( ( ph /\ m e. NN ) -> X e. Fin )
28 f1of 
 |-  ( F : NN -1-1-onto-> ( NN X. NN ) -> F : NN --> ( NN X. NN ) )
29 10 28 syl 
 |-  ( ph -> F : NN --> ( NN X. NN ) )
30 29 adantr 
 |-  ( ( ph /\ m e. NN ) -> F : NN --> ( NN X. NN ) )
31 simpr 
 |-  ( ( ph /\ m e. NN ) -> m e. NN )
32 30 31 ffvelrnd 
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) e. ( NN X. NN ) )
33 xp1st 
 |-  ( ( F ` m ) e. ( NN X. NN ) -> ( 1st ` ( F ` m ) ) e. NN )
34 32 33 syl 
 |-  ( ( ph /\ m e. NN ) -> ( 1st ` ( F ` m ) ) e. NN )
35 xp2nd 
 |-  ( ( F ` m ) e. ( NN X. NN ) -> ( 2nd ` ( F ` m ) ) e. NN )
36 32 35 syl 
 |-  ( ( ph /\ m e. NN ) -> ( 2nd ` ( F ` m ) ) e. NN )
37 fvex 
 |-  ( 2nd ` ( F ` m ) ) e. _V
38 eleq1 
 |-  ( j = ( 2nd ` ( F ` m ) ) -> ( j e. NN <-> ( 2nd ` ( F ` m ) ) e. NN ) )
39 38 3anbi3d 
 |-  ( j = ( 2nd ` ( F ` m ) ) -> ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) <-> ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ ( 2nd ` ( F ` m ) ) e. NN ) ) )
40 fveq2 
 |-  ( j = ( 2nd ` ( F ` m ) ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )
41 40 feq1d 
 |-  ( j = ( 2nd ` ( F ` m ) ) -> ( ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) ) )
42 39 41 imbi12d 
 |-  ( j = ( 2nd ` ( F ` m ) ) -> ( ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) ) <-> ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ ( 2nd ` ( F ` m ) ) e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) ) ) )
43 fvex 
 |-  ( 1st ` ( F ` m ) ) e. _V
44 eleq1 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( n e. NN <-> ( 1st ` ( F ` m ) ) e. NN ) )
45 44 3anbi2d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( ( ph /\ n e. NN /\ j e. NN ) <-> ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) ) )
46 fveq2 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( I ` n ) = ( I ` ( 1st ` ( F ` m ) ) ) )
47 46 fveq1d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( ( I ` n ) ` j ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) )
48 47 feq1d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( ( ( I ` n ) ` j ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) ) )
49 45 48 imbi12d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) ) <-> ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) ) ) )
50 sseq1 
 |-  ( a = ( A ` n ) -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) <-> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) ) )
51 50 rabbidv 
 |-  ( a = ( A ` n ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )
52 ovex 
 |-  ( ( ( RR X. RR ) ^m X ) ^m NN ) e. _V
53 52 rabex 
 |-  { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } e. _V
54 53 a1i 
 |-  ( ( ph /\ n e. NN ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } e. _V )
55 6 51 14 54 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( C ` ( A ` n ) ) = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )
56 ssrab2 
 |-  { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN )
57 56 a1i 
 |-  ( ( ph /\ n e. NN ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) )
58 55 57 eqsstrd 
 |-  ( ( ph /\ n e. NN ) -> ( C ` ( A ` n ) ) C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) )
59 fveq2 
 |-  ( a = ( A ` n ) -> ( C ` a ) = ( C ` ( A ` n ) ) )
60 59 eleq2d 
 |-  ( a = ( A ` n ) -> ( i e. ( C ` a ) <-> i e. ( C ` ( A ` n ) ) ) )
61 fveq2 
 |-  ( a = ( A ` n ) -> ( ( voln* ` X ) ` a ) = ( ( voln* ` X ) ` ( A ` n ) ) )
62 61 oveq1d 
 |-  ( a = ( A ` n ) -> ( ( ( voln* ` X ) ` a ) +e e ) = ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) )
63 62 breq2d 
 |-  ( a = ( A ` n ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) ) )
64 60 63 anbi12d 
 |-  ( a = ( A ` n ) -> ( ( i e. ( C ` a ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) ) <-> ( i e. ( C ` ( A ` n ) ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) ) ) )
65 64 rabbidva2 
 |-  ( a = ( A ` n ) -> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } = { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } )
66 65 mpteq2dv 
 |-  ( a = ( A ` n ) -> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) = ( e e. RR+ |-> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) )
67 rpex 
 |-  RR+ e. _V
68 67 mptex 
 |-  ( e e. RR+ |-> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) e. _V
69 68 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( e e. RR+ |-> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) e. _V )
70 8 66 14 69 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( D ` ( A ` n ) ) = ( e e. RR+ |-> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } ) )
71 oveq2 
 |-  ( e = ( E / ( 2 ^ n ) ) -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) = ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) )
72 71 breq2d 
 |-  ( e = ( E / ( 2 ^ n ) ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) )
73 72 rabbidv 
 |-  ( e = ( E / ( 2 ^ n ) ) -> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } = { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } )
74 73 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ e = ( E / ( 2 ^ n ) ) ) -> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e e ) } = { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } )
75 4 adantr 
 |-  ( ( ph /\ n e. NN ) -> E e. RR+ )
76 2nn 
 |-  2 e. NN
77 76 a1i 
 |-  ( n e. NN -> 2 e. NN )
78 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
79 77 78 nnexpcld 
 |-  ( n e. NN -> ( 2 ^ n ) e. NN )
80 79 nnrpd 
 |-  ( n e. NN -> ( 2 ^ n ) e. RR+ )
81 80 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR+ )
82 75 81 rpdivcld 
 |-  ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. RR+ )
83 fvex 
 |-  ( C ` ( A ` n ) ) e. _V
84 83 rabex 
 |-  { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } e. _V
85 84 a1i 
 |-  ( ( ph /\ n e. NN ) -> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } e. _V )
86 70 74 82 85 fvmptd 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) = { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } )
87 ssrab2 
 |-  { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } C_ ( C ` ( A ` n ) )
88 87 a1i 
 |-  ( ( ph /\ n e. NN ) -> { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } C_ ( C ` ( A ` n ) ) )
89 86 88 eqsstrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) C_ ( C ` ( A ` n ) ) )
90 89 9 sseldd 
 |-  ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( C ` ( A ` n ) ) )
91 58 90 sseldd 
 |-  ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
92 elmapfn 
 |-  ( ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( I ` n ) Fn NN )
93 91 92 syl 
 |-  ( ( ph /\ n e. NN ) -> ( I ` n ) Fn NN )
94 elmapi 
 |-  ( ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( I ` n ) : NN --> ( ( RR X. RR ) ^m X ) )
95 91 94 syl 
 |-  ( ( ph /\ n e. NN ) -> ( I ` n ) : NN --> ( ( RR X. RR ) ^m X ) )
96 95 ffvelrnda 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) )
97 96 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. j e. NN ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) )
98 93 97 jca 
 |-  ( ( ph /\ n e. NN ) -> ( ( I ` n ) Fn NN /\ A. j e. NN ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) )
99 98 3adant3 
 |-  ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) Fn NN /\ A. j e. NN ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) )
100 ffnfv 
 |-  ( ( I ` n ) : NN --> ( ( RR X. RR ) ^m X ) <-> ( ( I ` n ) Fn NN /\ A. j e. NN ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) ) )
101 99 100 sylibr 
 |-  ( ( ph /\ n e. NN /\ j e. NN ) -> ( I ` n ) : NN --> ( ( RR X. RR ) ^m X ) )
102 simp3 
 |-  ( ( ph /\ n e. NN /\ j e. NN ) -> j e. NN )
103 101 102 ffvelrnd 
 |-  ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) )
104 elmapi 
 |-  ( ( ( I ` n ) ` j ) e. ( ( RR X. RR ) ^m X ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) )
105 103 104 syl 
 |-  ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) )
106 43 49 105 vtocl 
 |-  ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) : X --> ( RR X. RR ) )
107 37 42 106 vtocl 
 |-  ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN /\ ( 2nd ` ( F ` m ) ) e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) )
108 26 34 36 107 syl3anc 
 |-  ( ( ph /\ m e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) )
109 id 
 |-  ( m e. NN -> m e. NN )
110 fvex 
 |-  ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) e. _V
111 110 a1i 
 |-  ( m e. NN -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) e. _V )
112 11 fvmpt2 
 |-  ( ( m e. NN /\ ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) e. _V ) -> ( G ` m ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )
113 109 111 112 syl2anc 
 |-  ( m e. NN -> ( G ` m ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )
114 113 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )
115 114 feq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( G ` m ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) : X --> ( RR X. RR ) ) )
116 108 115 mpbird 
 |-  ( ( ph /\ m e. NN ) -> ( G ` m ) : X --> ( RR X. RR ) )
117 25 27 7 116 hoiprodcl2 
 |-  ( ( ph /\ m e. NN ) -> ( L ` ( G ` m ) ) e. ( 0 [,) +oo ) )
118 24 117 sselid 
 |-  ( ( ph /\ m e. NN ) -> ( L ` ( G ` m ) ) e. ( 0 [,] +oo ) )
119 21 23 118 sge0xrclmpt 
 |-  ( ph -> ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) e. RR* )
120 nfv 
 |-  F/ n ph
121 0xr 
 |-  0 e. RR*
122 121 a1i 
 |-  ( ( ph /\ n e. NN ) -> 0 e. RR* )
123 pnfxr 
 |-  +oo e. RR*
124 123 a1i 
 |-  ( ( ph /\ n e. NN ) -> +oo e. RR* )
125 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. Fin )
126 125 16 5 ovnval2b 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) = if ( X = (/) , 0 , inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) )
127 2 neneqd 
 |-  ( ph -> -. X = (/) )
128 127 iffalsed 
 |-  ( ph -> if ( X = (/) , 0 , inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) = inf ( ( Z ` ( A ` n ) ) , RR* , < ) )
129 128 adantr 
 |-  ( ( ph /\ n e. NN ) -> if ( X = (/) , 0 , inf ( ( Z ` ( A ` n ) ) , RR* , < ) ) = inf ( ( Z ` ( A ` n ) ) , RR* , < ) )
130 126 129 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) = inf ( ( Z ` ( A ` n ) ) , RR* , < ) )
131 sseq1 
 |-  ( a = ( A ` n ) -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) <-> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) )
132 131 anbi1d 
 |-  ( a = ( A ` n ) -> ( ( 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 ) ) ) ) ) <-> ( ( A ` n ) 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 ) ) ) ) ) ) )
133 132 rexbidv 
 |-  ( a = ( A ` n ) -> ( 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 ) ) ) ) ) <-> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) 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 ) ) ) ) ) ) )
134 133 rabbidv 
 |-  ( a = ( A ` n ) -> { 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 ) ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) 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 ) ) ) ) ) } )
135 xrex 
 |-  RR* e. _V
136 135 rabex 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) 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 ) ) ) ) ) } e. _V
137 136 a1i 
 |-  ( ( ph /\ n e. NN ) -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) 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 ) ) ) ) ) } e. _V )
138 5 134 14 137 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( Z ` ( A ` n ) ) = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) 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 ) ) ) ) ) } )
139 ssrab2 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) 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 ) ) ) ) ) } C_ RR*
140 139 a1i 
 |-  ( ( ph /\ n e. NN ) -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( ( A ` n ) 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 ) ) ) ) ) } C_ RR* )
141 138 140 eqsstrd 
 |-  ( ( ph /\ n e. NN ) -> ( Z ` ( A ` n ) ) C_ RR* )
142 infxrcl 
 |-  ( ( Z ` ( A ` n ) ) C_ RR* -> inf ( ( Z ` ( A ` n ) ) , RR* , < ) e. RR* )
143 141 142 syl 
 |-  ( ( ph /\ n e. NN ) -> inf ( ( Z ` ( A ` n ) ) , RR* , < ) e. RR* )
144 130 143 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) e. RR* )
145 4 rpred 
 |-  ( ph -> E e. RR )
146 145 adantr 
 |-  ( ( ph /\ n e. NN ) -> E e. RR )
147 2re 
 |-  2 e. RR
148 147 a1i 
 |-  ( n e. NN -> 2 e. RR )
149 148 78 reexpcld 
 |-  ( n e. NN -> ( 2 ^ n ) e. RR )
150 149 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR )
151 148 recnd 
 |-  ( n e. NN -> 2 e. CC )
152 2ne0 
 |-  2 =/= 0
153 152 a1i 
 |-  ( n e. NN -> 2 =/= 0 )
154 nnz 
 |-  ( n e. NN -> n e. ZZ )
155 151 153 154 expne0d 
 |-  ( n e. NN -> ( 2 ^ n ) =/= 0 )
156 155 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) =/= 0 )
157 146 150 156 redivcld 
 |-  ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. RR )
158 157 rexrd 
 |-  ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. RR* )
159 144 158 xaddcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) e. RR* )
160 125 16 ovncl 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) e. ( 0 [,] +oo ) )
161 xrge0ge0 
 |-  ( ( ( voln* ` X ) ` ( A ` n ) ) e. ( 0 [,] +oo ) -> 0 <_ ( ( voln* ` X ) ` ( A ` n ) ) )
162 160 161 syl 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( ( voln* ` X ) ` ( A ` n ) ) )
163 0red 
 |-  ( ( ph /\ n e. NN ) -> 0 e. RR )
164 82 rpgt0d 
 |-  ( ( ph /\ n e. NN ) -> 0 < ( E / ( 2 ^ n ) ) )
165 163 157 164 ltled 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( E / ( 2 ^ n ) ) )
166 157 ltpnfd 
 |-  ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) < +oo )
167 158 124 166 xrltled 
 |-  ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) <_ +oo )
168 122 124 158 165 167 eliccxrd 
 |-  ( ( ph /\ n e. NN ) -> ( E / ( 2 ^ n ) ) e. ( 0 [,] +oo ) )
169 144 168 xadd0ge 
 |-  ( ( ph /\ n e. NN ) -> ( ( voln* ` X ) ` ( A ` n ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) )
170 122 144 159 162 169 xrletrd 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) )
171 pnfge 
 |-  ( ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) e. RR* -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) <_ +oo )
172 159 171 syl 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) <_ +oo )
173 122 124 159 170 172 eliccxrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) e. ( 0 [,] +oo ) )
174 120 23 173 sge0xrclmpt 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) e. RR* )
175 sseq1 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) <-> ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) ) )
176 175 rabbidv 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )
177 3 adantr 
 |-  ( ( ph /\ m e. NN ) -> A : NN --> ~P ( RR ^m X ) )
178 177 34 ffvelrnd 
 |-  ( ( ph /\ m e. NN ) -> ( A ` ( 1st ` ( F ` m ) ) ) e. ~P ( RR ^m X ) )
179 52 rabex 
 |-  { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } e. _V
180 179 a1i 
 |-  ( ( ph /\ m e. NN ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } e. _V )
181 6 176 178 180 fvmptd3 
 |-  ( ( ph /\ m e. NN ) -> ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )
182 ssrab2 
 |-  { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN )
183 182 a1i 
 |-  ( ( ph /\ m e. NN ) -> { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` ( 1st ` ( F ` m ) ) ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) )
184 181 183 eqsstrd 
 |-  ( ( ph /\ m e. NN ) -> ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) )
185 fveq2 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( C ` a ) = ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) )
186 185 eleq2d 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( i e. ( C ` a ) <-> i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) ) )
187 fveq2 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( ( voln* ` X ) ` a ) = ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) )
188 187 oveq1d 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( ( ( voln* ` X ) ` a ) +e e ) = ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) )
189 188 breq2d 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) ) )
190 186 189 anbi12d 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( ( i e. ( C ` a ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) ) <-> ( i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) ) ) )
191 190 rabbidva2 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } = { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } )
192 191 mpteq2dv 
 |-  ( a = ( A ` ( 1st ` ( F ` m ) ) ) -> ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } ) = ( e e. RR+ |-> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) )
193 67 mptex 
 |-  ( e e. RR+ |-> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) e. _V
194 193 a1i 
 |-  ( ( ph /\ m e. NN ) -> ( e e. RR+ |-> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) e. _V )
195 8 192 178 194 fvmptd3 
 |-  ( ( ph /\ m e. NN ) -> ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) = ( e e. RR+ |-> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } ) )
196 oveq2 
 |-  ( e = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) -> ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) = ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) )
197 196 breq2d 
 |-  ( e = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) )
198 197 rabbidv 
 |-  ( e = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) -> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } = { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } )
199 198 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ e = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) -> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e e ) } = { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } )
200 26 4 syl 
 |-  ( ( ph /\ m e. NN ) -> E e. RR+ )
201 2rp 
 |-  2 e. RR+
202 201 a1i 
 |-  ( ( ph /\ m e. NN ) -> 2 e. RR+ )
203 34 nnzd 
 |-  ( ( ph /\ m e. NN ) -> ( 1st ` ( F ` m ) ) e. ZZ )
204 202 203 rpexpcld 
 |-  ( ( ph /\ m e. NN ) -> ( 2 ^ ( 1st ` ( F ` m ) ) ) e. RR+ )
205 200 204 rpdivcld 
 |-  ( ( ph /\ m e. NN ) -> ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) e. RR+ )
206 fvex 
 |-  ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) e. _V
207 206 rabex 
 |-  { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } e. _V
208 207 a1i 
 |-  ( ( ph /\ m e. NN ) -> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } e. _V )
209 195 199 205 208 fvmptd 
 |-  ( ( ph /\ m e. NN ) -> ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) = { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } )
210 ssrab2 
 |-  { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } C_ ( C ` ( A ` ( 1st ` ( F ` m ) ) ) )
211 210 a1i 
 |-  ( ( ph /\ m e. NN ) -> { i e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` ( 1st ` ( F ` m ) ) ) ) +e ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) } C_ ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) )
212 209 211 eqsstrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) C_ ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) )
213 44 anbi2d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( ( ph /\ n e. NN ) <-> ( ph /\ ( 1st ` ( F ` m ) ) e. NN ) ) )
214 2fveq3 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( D ` ( A ` n ) ) = ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) )
215 oveq2 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( 2 ^ n ) = ( 2 ^ ( 1st ` ( F ` m ) ) ) )
216 215 oveq2d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( E / ( 2 ^ n ) ) = ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) )
217 214 216 fveq12d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) = ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) )
218 46 217 eleq12d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( ( I ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) <-> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) )
219 213 218 imbi12d 
 |-  ( n = ( 1st ` ( F ` m ) ) -> ( ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( ( D ` ( A ` n ) ) ` ( E / ( 2 ^ n ) ) ) ) <-> ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) ) ) )
220 43 219 9 vtocl 
 |-  ( ( ph /\ ( 1st ` ( F ` m ) ) e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) )
221 26 34 220 syl2anc 
 |-  ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( D ` ( A ` ( 1st ` ( F ` m ) ) ) ) ` ( E / ( 2 ^ ( 1st ` ( F ` m ) ) ) ) ) )
222 212 221 sseldd 
 |-  ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( C ` ( A ` ( 1st ` ( F ` m ) ) ) ) )
223 184 222 sseldd 
 |-  ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
224 elmapfn 
 |-  ( ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) Fn NN )
225 223 224 syl 
 |-  ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) Fn NN )
226 elmapi 
 |-  ( ( I ` ( 1st ` ( F ` m ) ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) : NN --> ( ( RR X. RR ) ^m X ) )
227 223 226 syl 
 |-  ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) : NN --> ( ( RR X. RR ) ^m X ) )
228 227 ffvelrnda 
 |-  ( ( ( ph /\ m e. NN ) /\ j e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) e. ( ( RR X. RR ) ^m X ) )
229 228 ralrimiva 
 |-  ( ( ph /\ m e. NN ) -> A. j e. NN ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) e. ( ( RR X. RR ) ^m X ) )
230 225 229 jca 
 |-  ( ( ph /\ m e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) Fn NN /\ A. j e. NN ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) e. ( ( RR X. RR ) ^m X ) ) )
231 ffnfv 
 |-  ( ( I ` ( 1st ` ( F ` m ) ) ) : NN --> ( ( RR X. RR ) ^m X ) <-> ( ( I ` ( 1st ` ( F ` m ) ) ) Fn NN /\ A. j e. NN ( ( I ` ( 1st ` ( F ` m ) ) ) ` j ) e. ( ( RR X. RR ) ^m X ) ) )
232 230 231 sylibr 
 |-  ( ( ph /\ m e. NN ) -> ( I ` ( 1st ` ( F ` m ) ) ) : NN --> ( ( RR X. RR ) ^m X ) )
233 232 36 ffvelrnd 
 |-  ( ( ph /\ m e. NN ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) e. ( ( RR X. RR ) ^m X ) )
234 233 11 fmptd 
 |-  ( ph -> G : NN --> ( ( RR X. RR ) ^m X ) )
235 simpl 
 |-  ( ( ph /\ n e. NN ) -> ph )
236 9 86 eleqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( I ` n ) e. { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } )
237 87 236 sselid 
 |-  ( ( ph /\ n e. NN ) -> ( I ` n ) e. ( C ` ( A ` n ) ) )
238 simp3 
 |-  ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( I ` n ) e. ( C ` ( A ` n ) ) )
239 55 3adant3 
 |-  ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( C ` ( A ` n ) ) = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )
240 238 239 eleqtrd 
 |-  ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( I ` n ) e. { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } )
241 fveq1 
 |-  ( h = ( I ` n ) -> ( h ` j ) = ( ( I ` n ) ` j ) )
242 241 coeq2d 
 |-  ( h = ( I ` n ) -> ( [,) o. ( h ` j ) ) = ( [,) o. ( ( I ` n ) ` j ) ) )
243 242 fveq1d 
 |-  ( h = ( I ` n ) -> ( ( [,) o. ( h ` j ) ) ` k ) = ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) )
244 243 ixpeq2dv 
 |-  ( h = ( I ` n ) -> X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) )
245 244 iuneq2d 
 |-  ( h = ( I ` n ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) )
246 245 sseq2d 
 |-  ( h = ( I ` n ) -> ( ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) <-> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) )
247 246 elrab 
 |-  ( ( I ` n ) e. { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) } <-> ( ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) )
248 240 247 sylib 
 |-  ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( ( I ` n ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) ) )
249 248 simprd 
 |-  ( ( ph /\ n e. NN /\ ( I ` n ) e. ( C ` ( A ` n ) ) ) -> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) )
250 235 13 237 249 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) )
251 f1ofo 
 |-  ( F : NN -1-1-onto-> ( NN X. NN ) -> F : NN -onto-> ( NN X. NN ) )
252 10 251 syl 
 |-  ( ph -> F : NN -onto-> ( NN X. NN ) )
253 252 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> F : NN -onto-> ( NN X. NN ) )
254 opelxpi 
 |-  ( ( n e. NN /\ j e. NN ) -> <. n , j >. e. ( NN X. NN ) )
255 13 254 sylan 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> <. n , j >. e. ( NN X. NN ) )
256 foelrni 
 |-  ( ( F : NN -onto-> ( NN X. NN ) /\ <. n , j >. e. ( NN X. NN ) ) -> E. m e. NN ( F ` m ) = <. n , j >. )
257 253 255 256 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> E. m e. NN ( F ` m ) = <. n , j >. )
258 nfv 
 |-  F/ m ( ( ph /\ n e. NN ) /\ j e. NN )
259 nfre1 
 |-  F/ m E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k )
260 simpl 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> m e. NN )
261 fveq2 
 |-  ( ( F ` m ) = <. n , j >. -> ( 1st ` ( F ` m ) ) = ( 1st ` <. n , j >. ) )
262 op1stg 
 |-  ( ( n e. _V /\ j e. _V ) -> ( 1st ` <. n , j >. ) = n )
263 262 el2v 
 |-  ( 1st ` <. n , j >. ) = n
264 263 a1i 
 |-  ( ( F ` m ) = <. n , j >. -> ( 1st ` <. n , j >. ) = n )
265 261 264 eqtrd 
 |-  ( ( F ` m ) = <. n , j >. -> ( 1st ` ( F ` m ) ) = n )
266 265 adantl 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( 1st ` ( F ` m ) ) = n )
267 260 266 jca 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( m e. NN /\ ( 1st ` ( F ` m ) ) = n ) )
268 2fveq3 
 |-  ( i = m -> ( 1st ` ( F ` i ) ) = ( 1st ` ( F ` m ) ) )
269 268 eqeq1d 
 |-  ( i = m -> ( ( 1st ` ( F ` i ) ) = n <-> ( 1st ` ( F ` m ) ) = n ) )
270 269 elrab 
 |-  ( m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } <-> ( m e. NN /\ ( 1st ` ( F ` m ) ) = n ) )
271 267 270 sylibr 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } )
272 271 3adant1 
 |-  ( ( ( ( ph /\ n e. NN ) /\ j e. NN ) /\ m e. NN /\ ( F ` m ) = <. n , j >. ) -> m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } )
273 260 113 syl 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( G ` m ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )
274 265 fveq2d 
 |-  ( ( F ` m ) = <. n , j >. -> ( I ` ( 1st ` ( F ` m ) ) ) = ( I ` n ) )
275 vex 
 |-  n e. _V
276 vex 
 |-  j e. _V
277 275 276 op2ndd 
 |-  ( ( F ` m ) = <. n , j >. -> ( 2nd ` ( F ` m ) ) = j )
278 274 277 fveq12d 
 |-  ( ( F ` m ) = <. n , j >. -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) = ( ( I ` n ) ` j ) )
279 278 adantl 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) = ( ( I ` n ) ` j ) )
280 273 279 eqtr2d 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( ( I ` n ) ` j ) = ( G ` m ) )
281 280 coeq2d 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( [,) o. ( ( I ` n ) ` j ) ) = ( [,) o. ( G ` m ) ) )
282 281 fveq1d 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) = ( ( [,) o. ( G ` m ) ) ` k ) )
283 282 ixpeq2dv 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
284 eqimss 
 |-  ( X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) -> X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
285 283 284 syl 
 |-  ( ( m e. NN /\ ( F ` m ) = <. n , j >. ) -> X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
286 285 3adant1 
 |-  ( ( ( ( ph /\ n e. NN ) /\ j e. NN ) /\ m e. NN /\ ( F ` m ) = <. n , j >. ) -> X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
287 rspe 
 |-  ( ( m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } /\ X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
288 272 286 287 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ j e. NN ) /\ m e. NN /\ ( F ` m ) = <. n , j >. ) -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
289 288 3exp 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( m e. NN -> ( ( F ` m ) = <. n , j >. -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) ) )
290 258 259 289 rexlimd 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( E. m e. NN ( F ` m ) = <. n , j >. -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) ) )
291 257 290 mpd 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
292 291 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. j e. NN E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
293 iunss2 
 |-  ( A. j e. NN E. m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
294 292 293 syl 
 |-  ( ( ph /\ n e. NN ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( ( I ` n ) ` j ) ) ` k ) C_ U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
295 250 294 sstrd 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) C_ U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
296 ssrab2 
 |-  { i e. NN | ( 1st ` ( F ` i ) ) = n } C_ NN
297 iunss1 
 |-  ( { i e. NN | ( 1st ` ( F ` i ) ) = n } C_ NN -> U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
298 296 297 ax-mp 
 |-  U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k )
299 298 a1i 
 |-  ( ( ph /\ n e. NN ) -> U_ m e. { i e. NN | ( 1st ` ( F ` i ) ) = n } X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
300 295 299 sstrd 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
301 300 ralrimiva 
 |-  ( ph -> A. n e. NN ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
302 iunss 
 |-  ( U_ n e. NN ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) <-> A. n e. NN ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
303 301 302 sylibr 
 |-  ( ph -> U_ n e. NN ( A ` n ) C_ U_ m e. NN X_ k e. X ( ( [,) o. ( G ` m ) ) ` k ) )
304 1 2 7 234 303 ovnlecvr 
 |-  ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) )
305 114 fveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( L ` ( G ` m ) ) = ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) )
306 305 mpteq2dva 
 |-  ( ph -> ( m e. NN |-> ( L ` ( G ` m ) ) ) = ( m e. NN |-> ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) ) )
307 306 fveq2d 
 |-  ( ph -> ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) = ( sum^ ` ( m e. NN |-> ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) ) ) )
308 nfv 
 |-  F/ p ph
309 2fveq3 
 |-  ( p = ( F ` m ) -> ( I ` ( 1st ` p ) ) = ( I ` ( 1st ` ( F ` m ) ) ) )
310 fveq2 
 |-  ( p = ( F ` m ) -> ( 2nd ` p ) = ( 2nd ` ( F ` m ) ) )
311 309 310 fveq12d 
 |-  ( p = ( F ` m ) -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) = ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) )
312 311 fveq2d 
 |-  ( p = ( F ` m ) -> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) = ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) )
313 eqidd 
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) = ( F ` m ) )
314 nfv 
 |-  F/ k ( ph /\ p e. ( NN X. NN ) )
315 1 adantr 
 |-  ( ( ph /\ p e. ( NN X. NN ) ) -> X e. Fin )
316 simpl 
 |-  ( ( ph /\ p e. ( NN X. NN ) ) -> ph )
317 xp1st 
 |-  ( p e. ( NN X. NN ) -> ( 1st ` p ) e. NN )
318 317 adantl 
 |-  ( ( ph /\ p e. ( NN X. NN ) ) -> ( 1st ` p ) e. NN )
319 xp2nd 
 |-  ( p e. ( NN X. NN ) -> ( 2nd ` p ) e. NN )
320 319 adantl 
 |-  ( ( ph /\ p e. ( NN X. NN ) ) -> ( 2nd ` p ) e. NN )
321 fvex 
 |-  ( 2nd ` p ) e. _V
322 eleq1 
 |-  ( j = ( 2nd ` p ) -> ( j e. NN <-> ( 2nd ` p ) e. NN ) )
323 322 3anbi3d 
 |-  ( j = ( 2nd ` p ) -> ( ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) <-> ( ph /\ ( 1st ` p ) e. NN /\ ( 2nd ` p ) e. NN ) ) )
324 fveq2 
 |-  ( j = ( 2nd ` p ) -> ( ( I ` ( 1st ` p ) ) ` j ) = ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) )
325 324 feq1d 
 |-  ( j = ( 2nd ` p ) -> ( ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) : X --> ( RR X. RR ) ) )
326 323 325 imbi12d 
 |-  ( j = ( 2nd ` p ) -> ( ( ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) ) <-> ( ( ph /\ ( 1st ` p ) e. NN /\ ( 2nd ` p ) e. NN ) -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) : X --> ( RR X. RR ) ) ) )
327 fvex 
 |-  ( 1st ` p ) e. _V
328 eleq1 
 |-  ( n = ( 1st ` p ) -> ( n e. NN <-> ( 1st ` p ) e. NN ) )
329 328 3anbi2d 
 |-  ( n = ( 1st ` p ) -> ( ( ph /\ n e. NN /\ j e. NN ) <-> ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) ) )
330 fveq2 
 |-  ( n = ( 1st ` p ) -> ( I ` n ) = ( I ` ( 1st ` p ) ) )
331 330 fveq1d 
 |-  ( n = ( 1st ` p ) -> ( ( I ` n ) ` j ) = ( ( I ` ( 1st ` p ) ) ` j ) )
332 331 feq1d 
 |-  ( n = ( 1st ` p ) -> ( ( ( I ` n ) ` j ) : X --> ( RR X. RR ) <-> ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) ) )
333 329 332 imbi12d 
 |-  ( n = ( 1st ` p ) -> ( ( ( ph /\ n e. NN /\ j e. NN ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) ) <-> ( ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) ) ) )
334 327 333 105 vtocl 
 |-  ( ( ph /\ ( 1st ` p ) e. NN /\ j e. NN ) -> ( ( I ` ( 1st ` p ) ) ` j ) : X --> ( RR X. RR ) )
335 321 326 334 vtocl 
 |-  ( ( ph /\ ( 1st ` p ) e. NN /\ ( 2nd ` p ) e. NN ) -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) : X --> ( RR X. RR ) )
336 316 318 320 335 syl3anc 
 |-  ( ( ph /\ p e. ( NN X. NN ) ) -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) : X --> ( RR X. RR ) )
337 314 315 7 336 hoiprodcl2 
 |-  ( ( ph /\ p e. ( NN X. NN ) ) -> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) e. ( 0 [,) +oo ) )
338 24 337 sselid 
 |-  ( ( ph /\ p e. ( NN X. NN ) ) -> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) e. ( 0 [,] +oo ) )
339 308 21 312 23 10 313 338 sge0f1o 
 |-  ( ph -> ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) = ( sum^ ` ( m e. NN |-> ( L ` ( ( I ` ( 1st ` ( F ` m ) ) ) ` ( 2nd ` ( F ` m ) ) ) ) ) ) )
340 307 339 eqtr4d 
 |-  ( ph -> ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) = ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) )
341 nfv 
 |-  F/ j ph
342 275 276 op1std 
 |-  ( p = <. n , j >. -> ( 1st ` p ) = n )
343 342 fveq2d 
 |-  ( p = <. n , j >. -> ( I ` ( 1st ` p ) ) = ( I ` n ) )
344 275 276 op2ndd 
 |-  ( p = <. n , j >. -> ( 2nd ` p ) = j )
345 343 344 fveq12d 
 |-  ( p = <. n , j >. -> ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) = ( ( I ` n ) ` j ) )
346 345 fveq2d 
 |-  ( p = <. n , j >. -> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) = ( L ` ( ( I ` n ) ` j ) ) )
347 nfv 
 |-  F/ k ( ( ph /\ n e. NN ) /\ j e. NN )
348 125 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> X e. Fin )
349 96 104 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( ( I ` n ) ` j ) : X --> ( RR X. RR ) )
350 347 348 7 349 hoiprodcl2 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( L ` ( ( I ` n ) ` j ) ) e. ( 0 [,) +oo ) )
351 24 350 sselid 
 |-  ( ( ( ph /\ n e. NN ) /\ j e. NN ) -> ( L ` ( ( I ` n ) ` j ) ) e. ( 0 [,] +oo ) )
352 351 3impa 
 |-  ( ( ph /\ n e. NN /\ j e. NN ) -> ( L ` ( ( I ` n ) ` j ) ) e. ( 0 [,] +oo ) )
353 341 346 23 23 352 sge0xp 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) ) ) = ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) )
354 353 eqcomd 
 |-  ( ph -> ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) = ( sum^ ` ( n e. NN |-> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) ) ) )
355 22 a1i 
 |-  ( ( ph /\ n e. NN ) -> NN e. _V )
356 eqid 
 |-  ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) = ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) )
357 351 356 fmptd 
 |-  ( ( ph /\ n e. NN ) -> ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) : NN --> ( 0 [,] +oo ) )
358 355 357 sge0cl 
 |-  ( ( ph /\ n e. NN ) -> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) e. ( 0 [,] +oo ) )
359 fveq1 
 |-  ( i = ( I ` n ) -> ( i ` j ) = ( ( I ` n ) ` j ) )
360 359 fveq2d 
 |-  ( i = ( I ` n ) -> ( L ` ( i ` j ) ) = ( L ` ( ( I ` n ) ` j ) ) )
361 360 mpteq2dv 
 |-  ( i = ( I ` n ) -> ( j e. NN |-> ( L ` ( i ` j ) ) ) = ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) )
362 361 fveq2d 
 |-  ( i = ( I ` n ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) )
363 362 breq1d 
 |-  ( i = ( I ` n ) -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) )
364 363 elrab 
 |-  ( ( I ` n ) e. { i e. ( C ` ( A ` n ) ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) } <-> ( ( I ` n ) e. ( C ` ( A ` n ) ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) )
365 236 364 sylib 
 |-  ( ( ph /\ n e. NN ) -> ( ( I ` n ) e. ( C ` ( A ` n ) ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) )
366 365 simprd 
 |-  ( ( ph /\ n e. NN ) -> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) )
367 120 23 358 173 366 sge0lempt 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( sum^ ` ( j e. NN |-> ( L ` ( ( I ` n ) ` j ) ) ) ) ) ) <_ ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) )
368 354 367 eqbrtrd 
 |-  ( ph -> ( sum^ ` ( p e. ( NN X. NN ) |-> ( L ` ( ( I ` ( 1st ` p ) ) ` ( 2nd ` p ) ) ) ) ) <_ ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) )
369 340 368 eqbrtrd 
 |-  ( ph -> ( sum^ ` ( m e. NN |-> ( L ` ( G ` m ) ) ) ) <_ ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) )
370 20 119 174 304 369 xrletrd 
 |-  ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) )
371 120 23 160 168 sge0xadd 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) = ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e ( sum^ ` ( n e. NN |-> ( E / ( 2 ^ n ) ) ) ) ) )
372 121 a1i 
 |-  ( ph -> 0 e. RR* )
373 123 a1i 
 |-  ( ph -> +oo e. RR* )
374 145 rexrd 
 |-  ( ph -> E e. RR* )
375 4 rpge0d 
 |-  ( ph -> 0 <_ E )
376 145 ltpnfd 
 |-  ( ph -> E < +oo )
377 372 373 374 375 376 elicod 
 |-  ( ph -> E e. ( 0 [,) +oo ) )
378 377 sge0ad2en 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( E / ( 2 ^ n ) ) ) ) = E )
379 378 oveq2d 
 |-  ( ph -> ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e ( sum^ ` ( n e. NN |-> ( E / ( 2 ^ n ) ) ) ) ) = ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )
380 371 379 eqtrd 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( ( ( voln* ` X ) ` ( A ` n ) ) +e ( E / ( 2 ^ n ) ) ) ) ) = ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )
381 370 380 breqtrd 
 |-  ( ph -> ( ( voln* ` X ) ` U_ n e. NN ( A ` n ) ) <_ ( ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( A ` n ) ) ) ) +e E ) )