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