Metamath Proof Explorer

Theorem hoicvrrex

Description: Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses hoicvrrex.fi 
|- ( ph -> X e. Fin )
hoicvrrex.y 
|- ( ph -> Y C_ ( RR ^m X ) )
Assertion hoicvrrex 
|- ( ph -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoicvrrex.fi 
 |-  ( ph -> X e. Fin )
2 hoicvrrex.y 
 |-  ( ph -> Y C_ ( RR ^m X ) )
3 nnre 
 |-  ( j e. NN -> j e. RR )
4 3 renegcld 
 |-  ( j e. NN -> -u j e. RR )
5 opelxpi 
 |-  ( ( -u j e. RR /\ j e. RR ) -> <. -u j , j >. e. ( RR X. RR ) )
6 4 3 5 syl2anc 
 |-  ( j e. NN -> <. -u j , j >. e. ( RR X. RR ) )
7 6 ad2antlr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> <. -u j , j >. e. ( RR X. RR ) )
8 eqid 
 |-  ( k e. X |-> <. -u j , j >. ) = ( k e. X |-> <. -u j , j >. )
9 7 8 fmptd 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> <. -u j , j >. ) : X --> ( RR X. RR ) )
10 reex 
 |-  RR e. _V
11 10 10 xpex 
 |-  ( RR X. RR ) e. _V
12 11 a1i 
 |-  ( ph -> ( RR X. RR ) e. _V )
13 elmapg 
 |-  ( ( ( RR X. RR ) e. _V /\ X e. Fin ) -> ( ( k e. X |-> <. -u j , j >. ) e. ( ( RR X. RR ) ^m X ) <-> ( k e. X |-> <. -u j , j >. ) : X --> ( RR X. RR ) ) )
14 12 1 13 syl2anc 
 |-  ( ph -> ( ( k e. X |-> <. -u j , j >. ) e. ( ( RR X. RR ) ^m X ) <-> ( k e. X |-> <. -u j , j >. ) : X --> ( RR X. RR ) ) )
15 14 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( ( k e. X |-> <. -u j , j >. ) e. ( ( RR X. RR ) ^m X ) <-> ( k e. X |-> <. -u j , j >. ) : X --> ( RR X. RR ) ) )
16 9 15 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> <. -u j , j >. ) e. ( ( RR X. RR ) ^m X ) )
17 eqid 
 |-  ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) )
18 16 17 fmptd 
 |-  ( ph -> ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) : NN --> ( ( RR X. RR ) ^m X ) )
19 ovex 
 |-  ( ( RR X. RR ) ^m X ) e. _V
20 nnex 
 |-  NN e. _V
21 19 20 elmap 
 |-  ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) : NN --> ( ( RR X. RR ) ^m X ) )
22 18 21 sylibr 
 |-  ( ph -> ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
23 eqid 
 |-  ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) = ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) )
24 23 1 hoicvr 
 |-  ( ph -> ( RR ^m X ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
25 eqidd 
 |-  ( l = k -> <. -u j , j >. = <. -u j , j >. )
26 25 cbvmptv 
 |-  ( l e. X |-> <. -u j , j >. ) = ( k e. X |-> <. -u j , j >. )
27 26 mpteq2i 
 |-  ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) )
28 27 a1i 
 |-  ( ph -> ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) )
29 28 fveq1d 
 |-  ( ph -> ( ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) ` j ) = ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) )
30 29 coeq2d 
 |-  ( ph -> ( [,) o. ( ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) ` j ) ) = ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) )
31 30 fveq1d 
 |-  ( ph -> ( ( [,) o. ( ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) = ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
32 31 ixpeq2dv 
 |-  ( ph -> X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
33 32 iuneq2d 
 |-  ( ph -> U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( l e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
34 24 33 sseqtrd 
 |-  ( ph -> ( RR ^m X ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
35 2 34 sstrd 
 |-  ( ph -> Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
36 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
37 16 elexd 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> <. -u j , j >. ) e. _V )
38 17 fvmpt2 
 |-  ( ( j e. NN /\ ( k e. X |-> <. -u j , j >. ) e. _V ) -> ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) = ( k e. X |-> <. -u j , j >. ) )
39 36 37 38 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) = ( k e. X |-> <. -u j , j >. ) )
40 39 7 fmpt3d 
 |-  ( ( ph /\ j e. NN ) -> ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) : X --> ( RR X. RR ) )
41 40 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) : X --> ( RR X. RR ) )
42 simpr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> k e. X )
43 41 42 fvovco 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) = ( ( 1st ` ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) ) [,) ( 2nd ` ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) ) ) )
44 39 fveq1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) = ( ( k e. X |-> <. -u j , j >. ) ` k ) )
45 44 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) = ( ( k e. X |-> <. -u j , j >. ) ` k ) )
46 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
47 opex 
 |-  <. -u j , j >. e. _V
48 47 a1i 
 |-  ( ( ph /\ k e. X ) -> <. -u j , j >. e. _V )
49 8 fvmpt2 
 |-  ( ( k e. X /\ <. -u j , j >. e. _V ) -> ( ( k e. X |-> <. -u j , j >. ) ` k ) = <. -u j , j >. )
50 46 48 49 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( k e. X |-> <. -u j , j >. ) ` k ) = <. -u j , j >. )
51 50 adantlr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( k e. X |-> <. -u j , j >. ) ` k ) = <. -u j , j >. )
52 45 51 eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) = <. -u j , j >. )
53 52 fveq2d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) ) = ( 1st ` <. -u j , j >. ) )
54 negex 
 |-  -u j e. _V
55 vex 
 |-  j e. _V
56 54 55 op1st 
 |-  ( 1st ` <. -u j , j >. ) = -u j
57 56 a1i 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` <. -u j , j >. ) = -u j )
58 53 57 eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) ) = -u j )
59 52 fveq2d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) ) = ( 2nd ` <. -u j , j >. ) )
60 54 55 op2nd 
 |-  ( 2nd ` <. -u j , j >. ) = j
61 60 a1i 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` <. -u j , j >. ) = j )
62 59 61 eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) ) = j )
63 58 62 oveq12d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( 1st ` ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) ) [,) ( 2nd ` ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ` k ) ) ) = ( -u j [,) j ) )
64 43 63 eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) = ( -u j [,) j ) )
65 64 fveq2d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) = ( vol ` ( -u j [,) j ) ) )
66 volico 
 |-  ( ( -u j e. RR /\ j e. RR ) -> ( vol ` ( -u j [,) j ) ) = if ( -u j < j , ( j - -u j ) , 0 ) )
67 4 3 66 syl2anc 
 |-  ( j e. NN -> ( vol ` ( -u j [,) j ) ) = if ( -u j < j , ( j - -u j ) , 0 ) )
68 nnrp 
 |-  ( j e. NN -> j e. RR+ )
69 neglt 
 |-  ( j e. RR+ -> -u j < j )
70 68 69 syl 
 |-  ( j e. NN -> -u j < j )
71 70 iftrued 
 |-  ( j e. NN -> if ( -u j < j , ( j - -u j ) , 0 ) = ( j - -u j ) )
72 3 recnd 
 |-  ( j e. NN -> j e. CC )
73 72 72 subnegd 
 |-  ( j e. NN -> ( j - -u j ) = ( j + j ) )
74 72 2timesd 
 |-  ( j e. NN -> ( 2 x. j ) = ( j + j ) )
75 73 74 eqtr4d 
 |-  ( j e. NN -> ( j - -u j ) = ( 2 x. j ) )
76 67 71 75 3eqtrd 
 |-  ( j e. NN -> ( vol ` ( -u j [,) j ) ) = ( 2 x. j ) )
77 76 ad2antlr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( -u j [,) j ) ) = ( 2 x. j ) )
78 65 77 eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) = ( 2 x. j ) )
79 78 prodeq2dv 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) = prod_ k e. X ( 2 x. j ) )
80 1 adantr 
 |-  ( ( ph /\ j e. NN ) -> X e. Fin )
81 2cnd 
 |-  ( ( ph /\ j e. NN ) -> 2 e. CC )
82 72 adantl 
 |-  ( ( ph /\ j e. NN ) -> j e. CC )
83 81 82 mulcld 
 |-  ( ( ph /\ j e. NN ) -> ( 2 x. j ) e. CC )
84 fprodconst 
 |-  ( ( X e. Fin /\ ( 2 x. j ) e. CC ) -> prod_ k e. X ( 2 x. j ) = ( ( 2 x. j ) ^ ( # ` X ) ) )
85 80 83 84 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( 2 x. j ) = ( ( 2 x. j ) ^ ( # ` X ) ) )
86 79 85 eqtrd 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) = ( ( 2 x. j ) ^ ( # ` X ) ) )
87 86 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) = ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) ) )
88 87 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) ) ) )
89 20 a1i 
 |-  ( ph -> NN e. _V )
90 68 ssriv 
 |-  NN C_ RR+
91 ioorp 
 |-  ( 0 (,) +oo ) = RR+
92 91 eqcomi 
 |-  RR+ = ( 0 (,) +oo )
93 90 92 sseqtri 
 |-  NN C_ ( 0 (,) +oo )
94 ioossicc 
 |-  ( 0 (,) +oo ) C_ ( 0 [,] +oo )
95 93 94 sstri 
 |-  NN C_ ( 0 [,] +oo )
96 2nn 
 |-  2 e. NN
97 96 a1i 
 |-  ( ( ph /\ j e. NN ) -> 2 e. NN )
98 97 36 nnmulcld 
 |-  ( ( ph /\ j e. NN ) -> ( 2 x. j ) e. NN )
99 hashcl 
 |-  ( X e. Fin -> ( # ` X ) e. NN0 )
100 1 99 syl 
 |-  ( ph -> ( # ` X ) e. NN0 )
101 100 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( # ` X ) e. NN0 )
102 nnexpcl 
 |-  ( ( ( 2 x. j ) e. NN /\ ( # ` X ) e. NN0 ) -> ( ( 2 x. j ) ^ ( # ` X ) ) e. NN )
103 98 101 102 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( 2 x. j ) ^ ( # ` X ) ) e. NN )
104 95 103 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( ( 2 x. j ) ^ ( # ` X ) ) e. ( 0 [,] +oo ) )
105 eqid 
 |-  ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) ) = ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) )
106 104 105 fmptd 
 |-  ( ph -> ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) ) : NN --> ( 0 [,] +oo ) )
107 89 106 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) ) ) e. RR* )
108 pnfxr 
 |-  +oo e. RR*
109 108 a1i 
 |-  ( ph -> +oo e. RR* )
110 1nn 
 |-  1 e. NN
111 95 110 sselii 
 |-  1 e. ( 0 [,] +oo )
112 111 a1i 
 |-  ( ( ph /\ j e. NN ) -> 1 e. ( 0 [,] +oo ) )
113 eqid 
 |-  ( j e. NN |-> 1 ) = ( j e. NN |-> 1 )
114 112 113 fmptd 
 |-  ( ph -> ( j e. NN |-> 1 ) : NN --> ( 0 [,] +oo ) )
115 89 114 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> 1 ) ) e. RR* )
116 nnnfi 
 |-  -. NN e. Fin
117 116 a1i 
 |-  ( ph -> -. NN e. Fin )
118 1rp 
 |-  1 e. RR+
119 118 a1i 
 |-  ( ph -> 1 e. RR+ )
120 89 117 119 sge0rpcpnf 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> 1 ) ) = +oo )
121 120 eqcomd 
 |-  ( ph -> +oo = ( sum^ ` ( j e. NN |-> 1 ) ) )
122 109 121 xreqled 
 |-  ( ph -> +oo <_ ( sum^ ` ( j e. NN |-> 1 ) ) )
123 nfv 
 |-  F/ j ph
124 114 fvmptelrn 
 |-  ( ( ph /\ j e. NN ) -> 1 e. ( 0 [,] +oo ) )
125 103 nnge1d 
 |-  ( ( ph /\ j e. NN ) -> 1 <_ ( ( 2 x. j ) ^ ( # ` X ) ) )
126 123 89 124 104 125 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> 1 ) ) <_ ( sum^ ` ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) ) ) )
127 109 115 107 122 126 xrletrd 
 |-  ( ph -> +oo <_ ( sum^ ` ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) ) ) )
128 107 127 xrgepnfd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( 2 x. j ) ^ ( # ` X ) ) ) ) = +oo )
129 eqidd 
 |-  ( ph -> +oo = +oo )
130 88 128 129 3eqtrrd 
 |-  ( ph -> +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) ) )
131 35 130 jca 
 |-  ( ph -> ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) /\ +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) ) ) )
132 nfcv 
 |-  F/_ j i
133 nfmpt1 
 |-  F/_ j ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) )
134 132 133 nfeq 
 |-  F/ j i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) )
135 nfcv 
 |-  F/_ k i
136 nfcv 
 |-  F/_ k NN
137 nfmpt1 
 |-  F/_ k ( k e. X |-> <. -u j , j >. )
138 136 137 nfmpt 
 |-  F/_ k ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) )
139 135 138 nfeq 
 |-  F/ k i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) )
140 fveq1 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( i ` j ) = ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) )
141 140 coeq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( [,) o. ( i ` j ) ) = ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) )
142 141 fveq1d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
143 142 adantr 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) /\ k e. X ) -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
144 139 143 ixpeq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
145 144 adantr 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) /\ j e. NN ) -> X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
146 134 145 iuneq2df 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) )
147 146 sseq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) <-> Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) )
148 142 fveq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) )
149 148 a1d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( k e. X -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) )
150 139 149 ralrimi 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> A. k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) )
151 150 adantr 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) /\ j e. NN ) -> A. k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) )
152 151 prodeq2d 
 |-  ( ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) )
153 134 152 mpteq2da 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) )
154 153 fveq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) ) )
155 154 eqeq2d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) ) ) )
156 147 155 anbi12d 
 |-  ( i = ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) -> ( ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) /\ +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) ) ) ) )
157 156 rspcev 
 |-  ( ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) /\ +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( ( j e. NN |-> ( k e. X |-> <. -u j , j >. ) ) ` j ) ) ` k ) ) ) ) ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
158 22 131 157 syl2anc 
 |-  ( ph -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( Y C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ +oo = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )