Metamath Proof Explorer

Theorem ovncvrrp

Description: The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovncvrrp.x 
|- ( ph -> X e. Fin )
ovncvrrp.n0 
|- ( ph -> X =/= (/) )
ovncvrrp.a 
|- ( ph -> A C_ ( RR ^m X ) )
ovncvrrp.e 
|- ( ph -> E e. RR+ )
ovncvrrp.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 ) } )
ovncvrrp.l 
|- L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
ovncvrrp.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 ovncvrrp 
|- ( ph -> E. i i e. ( ( D ` A ) ` E ) )

Proof

Step Hyp Ref Expression
1 ovncvrrp.x 
 |-  ( ph -> X e. Fin )
2 ovncvrrp.n0 
 |-  ( ph -> X =/= (/) )
3 ovncvrrp.a 
 |-  ( ph -> A C_ ( RR ^m X ) )
4 ovncvrrp.e 
 |-  ( ph -> E e. RR+ )
5 ovncvrrp.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 ) } )
6 ovncvrrp.l 
 |-  L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
7 ovncvrrp.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 ) } ) )
8 eqid 
 |-  { 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 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 ) ) ) ) ) }
9 1 2 3 4 8 ovnlerp 
 |-  ( ph -> E. z e. { 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 <_ ( ( ( voln* ` X ) ` A ) +e E ) )
10 simp1 
 |-  ( ( ph /\ z e. { 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 <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> ph )
11 simp3 
 |-  ( ( ph /\ z e. { 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 <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> z <_ ( ( ( voln* ` X ) ` A ) +e E ) )
12 rabid 
 |-  ( z e. { 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 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 ) ) ) ) ) ) )
13 12 biimpi 
 |-  ( z e. { 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 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 ) ) ) ) ) ) )
14 13 simprd 
 |-  ( z e. { 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 ) ) ) ) ) } -> 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 ) ) ) ) ) )
15 14 adantr 
 |-  ( ( z e. { 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 <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> 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 ) ) ) ) ) )
16 15 3adant1 
 |-  ( ( ph /\ z e. { 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 <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> 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 ) ) ) ) ) )
17 nfv 
 |-  F/ i ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) )
18 nfe1 
 |-  F/ i E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) )
19 simp1l 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e 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 ) ) ) ) ) ) -> ph )
20 simp2 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e 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 ) ) ) ) ) ) -> i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
21 simp3l 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e 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 ) ) ) ) ) ) -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
22 id 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) )
23 fveq1 
 |-  ( l = i -> ( l ` j ) = ( i ` j ) )
24 23 coeq2d 
 |-  ( l = i -> ( [,) o. ( l ` j ) ) = ( [,) o. ( i ` j ) ) )
25 24 fveq1d 
 |-  ( l = i -> ( ( [,) o. ( l ` j ) ) ` k ) = ( ( [,) o. ( i ` j ) ) ` k ) )
26 25 ixpeq2dv 
 |-  ( l = i -> X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
27 26 iuneq2d 
 |-  ( l = i -> U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
28 27 sseq2d 
 |-  ( l = i -> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) <-> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) )
29 28 elrab 
 |-  ( i e. { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } <-> ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) )
30 22 29 sylibr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> i e. { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
31 30 3adant1 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> i e. { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
32 sseq1 
 |-  ( a = A -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) <-> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) ) )
33 32 rabbidv 
 |-  ( a = A -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
34 ovexd 
 |-  ( ph -> ( RR ^m X ) e. _V )
35 34 3 ssexd 
 |-  ( ph -> A e. _V )
36 elpwg 
 |-  ( A e. _V -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) )
37 35 36 syl 
 |-  ( ph -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) )
38 3 37 mpbird 
 |-  ( ph -> A e. ~P ( RR ^m X ) )
39 ovex 
 |-  ( ( ( RR X. RR ) ^m X ) ^m NN ) e. _V
40 39 rabex 
 |-  { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } e. _V
41 40 a1i 
 |-  ( ph -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } e. _V )
42 5 33 38 41 fvmptd3 
 |-  ( ph -> ( C ` A ) = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
43 42 eqcomd 
 |-  ( ph -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } = ( C ` A ) )
44 43 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } = ( C ` A ) )
45 31 44 eleqtrd 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> i e. ( C ` A ) )
46 19 20 21 45 syl3anc 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e 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 ) ) ) ) ) ) -> i e. ( C ` A ) )
47 coeq2 
 |-  ( h = ( i ` j ) -> ( [,) o. h ) = ( [,) o. ( i ` j ) ) )
48 47 fveq1d 
 |-  ( h = ( i ` j ) -> ( ( [,) o. h ) ` k ) = ( ( [,) o. ( i ` j ) ) ` k ) )
49 48 fveq2d 
 |-  ( h = ( i ` j ) -> ( vol ` ( ( [,) o. h ) ` k ) ) = ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
50 49 prodeq2ad 
 |-  ( h = ( i ` j ) -> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
51 elmapi 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> i : NN --> ( ( RR X. RR ) ^m X ) )
52 51 adantr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> i : NN --> ( ( RR X. RR ) ^m X ) )
53 simpr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> j e. NN )
54 52 53 ffvelcdmd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> ( i ` j ) e. ( ( RR X. RR ) ^m X ) )
55 prodex 
 |-  prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) e. _V
56 55 a1i 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) e. _V )
57 6 50 54 56 fvmptd3 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> ( L ` ( i ` j ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
58 57 mpteq2dva 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( j e. NN |-> ( L ` ( i ` j ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
59 58 fveq2d 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
60 59 adantr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
61 id 
 |-  ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) -> z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
62 61 eqcomd 
 |-  ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = z )
63 62 adantl 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = z )
64 60 63 eqtrd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = z )
65 64 3adant1 
 |-  ( ( z <_ ( ( ( voln* ` X ) ` A ) +e E ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = z )
66 simp1 
 |-  ( ( z <_ ( ( ( voln* ` X ) ` A ) +e E ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> z <_ ( ( ( voln* ` X ) ` A ) +e E ) )
67 65 66 eqbrtrd 
 |-  ( ( z <_ ( ( ( voln* ` X ) ` A ) +e E ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) )
68 67 3adant1l 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) )
69 68 3adant3l 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e 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 ) ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) )
70 46 69 jca 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e 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 ) ) ) ) ) ) -> ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
71 70 19.8ad 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e 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 ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
72 71 3exp 
 |-  ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e 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 ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) ) )
73 17 18 72 rexlimd 
 |-  ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> ( 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 ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) )
74 73 imp 
 |-  ( ( ( ph /\ z <_ ( ( ( voln* ` X ) ` A ) +e E ) ) /\ 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 ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
75 10 11 16 74 syl21anc 
 |-  ( ( ph /\ z e. { 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 <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
76 75 3exp 
 |-  ( ph -> ( z e. { 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 <_ ( ( ( voln* ` X ) ` A ) +e E ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) ) )
77 76 rexlimdv 
 |-  ( ph -> ( E. z e. { 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 <_ ( ( ( voln* ` X ) ` A ) +e E ) -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) )
78 9 77 mpd 
 |-  ( ph -> E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
79 rabid 
 |-  ( i e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } <-> ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
80 79 bicomi 
 |-  ( ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) <-> i e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
81 80 biimpi 
 |-  ( ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> i e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
82 81 adantl 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> i e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
83 nfcv 
 |-  F/_ b ( e e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } )
84 nfcv 
 |-  F/_ a RR+
85 nfv 
 |-  F/ a ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e )
86 nfmpt1 
 |-  F/_ a ( 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 ) } )
87 5 86 nfcxfr 
 |-  F/_ a C
88 nfcv 
 |-  F/_ a b
89 87 88 nffv 
 |-  F/_ a ( C ` b )
90 85 89 nfrabw 
 |-  F/_ a { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) }
91 84 90 nfmpt 
 |-  F/_ a ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } )
92 fveq2 
 |-  ( a = b -> ( C ` a ) = ( C ` b ) )
93 92 eleq2d 
 |-  ( a = b -> ( i e. ( C ` a ) <-> i e. ( C ` b ) ) )
94 fveq2 
 |-  ( a = b -> ( ( voln* ` X ) ` a ) = ( ( voln* ` X ) ` b ) )
95 94 oveq1d 
 |-  ( a = b -> ( ( ( voln* ` X ) ` a ) +e e ) = ( ( ( voln* ` X ) ` b ) +e e ) )
96 95 breq2d 
 |-  ( a = b -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) ) )
97 93 96 anbi12d 
 |-  ( a = b -> ( ( i e. ( C ` a ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) ) <-> ( i e. ( C ` b ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) ) ) )
98 97 rabbidva2 
 |-  ( a = b -> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e e ) } = { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } )
99 98 mpteq2dv 
 |-  ( a = b -> ( 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 ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) )
100 83 91 99 cbvmpt 
 |-  ( 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 ) } ) ) = ( b e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) )
101 7 100 eqtri 
 |-  D = ( b e. ~P ( RR ^m X ) |-> ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) )
102 fveq2 
 |-  ( b = A -> ( C ` b ) = ( C ` A ) )
103 102 eleq2d 
 |-  ( b = A -> ( i e. ( C ` b ) <-> i e. ( C ` A ) ) )
104 fveq2 
 |-  ( b = A -> ( ( voln* ` X ) ` b ) = ( ( voln* ` X ) ` A ) )
105 104 oveq1d 
 |-  ( b = A -> ( ( ( voln* ` X ) ` b ) +e e ) = ( ( ( voln* ` X ) ` A ) +e e ) )
106 105 breq2d 
 |-  ( b = A -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) ) )
107 103 106 anbi12d 
 |-  ( b = A -> ( ( i e. ( C ` b ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) ) <-> ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) ) ) )
108 107 rabbidva2 
 |-  ( b = A -> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } )
109 108 mpteq2dv 
 |-  ( b = A -> ( e e. RR+ |-> { i e. ( C ` b ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e e ) } ) = ( e e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) )
110 38 adantr 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> A e. ~P ( RR ^m X ) )
111 rpex 
 |-  RR+ e. _V
112 111 mptex 
 |-  ( e e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) e. _V
113 112 a1i 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> ( e e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) e. _V )
114 101 109 110 113 fvmptd3 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> ( D ` A ) = ( e e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } ) )
115 oveq2 
 |-  ( e = E -> ( ( ( voln* ` X ) ` A ) +e e ) = ( ( ( voln* ` X ) ` A ) +e E ) )
116 115 breq2d 
 |-  ( e = E -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
117 116 rabbidv 
 |-  ( e = E -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
118 117 adantl 
 |-  ( ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) /\ e = E ) -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
119 4 adantr 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> E e. RR+ )
120 fvex 
 |-  ( C ` A ) e. _V
121 120 rabex 
 |-  { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } e. _V
122 121 a1i 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } e. _V )
123 114 118 119 122 fvmptd 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> ( ( D ` A ) ` E ) = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
124 123 eqcomd 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } = ( ( D ` A ) ` E ) )
125 82 124 eleqtrd 
 |-  ( ( ph /\ ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) ) -> i e. ( ( D ` A ) ` E ) )
126 125 ex 
 |-  ( ph -> ( ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> i e. ( ( D ` A ) ` E ) ) )
127 126 eximdv 
 |-  ( ph -> ( E. i ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) -> E. i i e. ( ( D ` A ) ` E ) ) )
128 78 127 mpd 
 |-  ( ph -> E. i i e. ( ( D ` A ) ` E ) )