Metamath Proof Explorer

Theorem hoicvr

Description: I is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020) Avoid ax-rep and shorten proof. (Revised by GG, 2-Apr-2026)

Ref Expression
Hypotheses hoicvr.2 
|- I = ( j e. NN |-> ( x e. X |-> <. -u j , j >. ) )
hoicvr.3 
|- ( ph -> X e. Fin )
Assertion hoicvr 
|- ( ph -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )

Proof

Step Hyp Ref Expression
1 hoicvr.2 
 |-  I = ( j e. NN |-> ( x e. X |-> <. -u j , j >. ) )
2 hoicvr.3 
 |-  ( ph -> X e. Fin )
3 reex 
 |-  RR e. _V
4 mapdm0 
 |-  ( RR e. _V -> ( RR ^m (/) ) = { (/) } )
5 3 4 ax-mp 
 |-  ( RR ^m (/) ) = { (/) }
6 oveq2 
 |-  ( X = (/) -> ( RR ^m X ) = ( RR ^m (/) ) )
7 ixpeq1 
 |-  ( X = (/) -> X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) = X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) )
8 7 iuneq2d 
 |-  ( X = (/) -> U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) = U_ j e. NN X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) )
9 ixp0x 
 |-  X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = { (/) }
10 9 a1i 
 |-  ( j e. NN -> X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = { (/) } )
11 10 iuneq2i 
 |-  U_ j e. NN X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = U_ j e. NN { (/) }
12 nnn0 
 |-  NN =/= (/)
13 iunconst 
 |-  ( NN =/= (/) -> U_ j e. NN { (/) } = { (/) } )
14 12 13 ax-mp 
 |-  U_ j e. NN { (/) } = { (/) }
15 11 14 eqtri 
 |-  U_ j e. NN X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = { (/) }
16 8 15 eqtrdi 
 |-  ( X = (/) -> U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) = { (/) } )
17 5 6 16 3eqtr4a 
 |-  ( X = (/) -> ( RR ^m X ) = U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
18 17 eqimssd 
 |-  ( X = (/) -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
19 18 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
20 elmapi 
 |-  ( f e. ( RR ^m X ) -> f : X --> RR )
21 20 adantl 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f : X --> RR )
22 21 ffnd 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f Fn X )
23 22 ad3antrrr 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f Fn X )
24 simplll 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( ph /\ f e. ( RR ^m X ) ) )
25 simpllr 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> j e. NN )
26 simplr 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> sup ( ran ( abs o. f ) , RR , < ) < j )
27 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> i e. X )
28 nnnegz 
 |-  ( j e. NN -> -u j e. ZZ )
29 28 zxrd 
 |-  ( j e. NN -> -u j e. RR* )
30 29 adantr 
 |-  ( ( j e. NN /\ i e. X ) -> -u j e. RR* )
31 30 3ad2antl2 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j e. RR* )
32 nnxr 
 |-  ( j e. NN -> j e. RR* )
33 32 adantr 
 |-  ( ( j e. NN /\ i e. X ) -> j e. RR* )
34 33 3ad2antl2 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> j e. RR* )
35 20 3ad2ant1 
 |-  ( ( f e. ( RR ^m X ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f : X --> RR )
36 35 frexr 
 |-  ( ( f e. ( RR ^m X ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f : X --> RR* )
37 36 3adant1l 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f : X --> RR* )
38 37 ffvelcdmda 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. RR* )
39 nnre 
 |-  ( j e. NN -> j e. RR )
40 39 adantr 
 |-  ( ( j e. NN /\ i e. X ) -> j e. RR )
41 40 3ad2antl2 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> j e. RR )
42 41 renegcld 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j e. RR )
43 21 ffvelcdmda 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ( f ` i ) e. RR )
44 43 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. RR )
45 44 renegcld 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u ( f ` i ) e. RR )
46 n0i 
 |-  ( i e. X -> -. X = (/) )
47 rncoss 
 |-  ran ( abs o. f ) C_ ran abs
48 absf 
 |-  abs : CC --> RR
49 frn 
 |-  ( abs : CC --> RR -> ran abs C_ RR )
50 48 49 ax-mp 
 |-  ran abs C_ RR
51 47 50 sstri 
 |-  ran ( abs o. f ) C_ RR
52 ltso 
 |-  < Or RR
53 52 a1i 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> < Or RR )
54 48 a1i 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> abs : CC --> RR )
55 ax-resscn 
 |-  RR C_ CC
56 55 a1i 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> RR C_ CC )
57 54 56 21 fcoss 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> ( abs o. f ) : X --> RR )
58 2 adantr 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> X e. Fin )
59 rnffi 
 |-  ( ( ( abs o. f ) : X --> RR /\ X e. Fin ) -> ran ( abs o. f ) e. Fin )
60 57 58 59 syl2anc 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> ran ( abs o. f ) e. Fin )
61 60 adantr 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> ran ( abs o. f ) e. Fin )
62 20 frnd 
 |-  ( f e. ( RR ^m X ) -> ran f C_ RR )
63 48 fdmi 
 |-  dom abs = CC
64 63 eqcomi 
 |-  CC = dom abs
65 55 64 sseqtri 
 |-  RR C_ dom abs
66 62 65 sstrdi 
 |-  ( f e. ( RR ^m X ) -> ran f C_ dom abs )
67 dmcosseq 
 |-  ( ran f C_ dom abs -> dom ( abs o. f ) = dom f )
68 66 67 syl 
 |-  ( f e. ( RR ^m X ) -> dom ( abs o. f ) = dom f )
69 20 fdmd 
 |-  ( f e. ( RR ^m X ) -> dom f = X )
70 68 69 eqtrd 
 |-  ( f e. ( RR ^m X ) -> dom ( abs o. f ) = X )
71 70 adantr 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> dom ( abs o. f ) = X )
72 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
73 72 adantl 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> X =/= (/) )
74 71 73 eqnetrd 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> dom ( abs o. f ) =/= (/) )
75 74 neneqd 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> -. dom ( abs o. f ) = (/) )
76 dm0rn0 
 |-  ( dom ( abs o. f ) = (/) <-> ran ( abs o. f ) = (/) )
77 75 76 sylnib 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> -. ran ( abs o. f ) = (/) )
78 77 neqned 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> ran ( abs o. f ) =/= (/) )
79 78 adantll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> ran ( abs o. f ) =/= (/) )
80 51 a1i 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> ran ( abs o. f ) C_ RR )
81 fisupcl 
 |-  ( ( < Or RR /\ ( ran ( abs o. f ) e. Fin /\ ran ( abs o. f ) =/= (/) /\ ran ( abs o. f ) C_ RR ) ) -> sup ( ran ( abs o. f ) , RR , < ) e. ran ( abs o. f ) )
82 53 61 79 80 81 syl13anc 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> sup ( ran ( abs o. f ) , RR , < ) e. ran ( abs o. f ) )
83 51 82 sselid 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> sup ( ran ( abs o. f ) , RR , < ) e. RR )
84 46 83 sylan2 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> sup ( ran ( abs o. f ) , RR , < ) e. RR )
85 84 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> sup ( ran ( abs o. f ) , RR , < ) e. RR )
86 20 ffvelcdmda 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( f ` i ) e. RR )
87 86 recnd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( f ` i ) e. CC )
88 87 abscld 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. RR )
89 88 adantll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. RR )
90 89 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. RR )
91 86 renegcld 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> -u ( f ` i ) e. RR )
92 91 leabsd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> -u ( f ` i ) <_ ( abs ` -u ( f ` i ) ) )
93 87 absnegd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( abs ` -u ( f ` i ) ) = ( abs ` ( f ` i ) ) )
94 92 93 breqtrd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> -u ( f ` i ) <_ ( abs ` ( f ` i ) ) )
95 94 adantll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> -u ( f ` i ) <_ ( abs ` ( f ` i ) ) )
96 95 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u ( f ` i ) <_ ( abs ` ( f ` i ) ) )
97 51 a1i 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ran ( abs o. f ) C_ RR )
98 46 79 sylan2 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ran ( abs o. f ) =/= (/) )
99 98 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ran ( abs o. f ) =/= (/) )
100 fimaxre2 
 |-  ( ( ran ( abs o. f ) C_ RR /\ ran ( abs o. f ) e. Fin ) -> E. y e. RR A. z e. ran ( abs o. f ) z <_ y )
101 51 60 100 sylancr 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> E. y e. RR A. z e. ran ( abs o. f ) z <_ y )
102 101 adantr 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> E. y e. RR A. z e. ran ( abs o. f ) z <_ y )
103 102 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> E. y e. RR A. z e. ran ( abs o. f ) z <_ y )
104 elmapfun 
 |-  ( f e. ( RR ^m X ) -> Fun f )
105 simpr 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> i e. X )
106 69 eqcomd 
 |-  ( f e. ( RR ^m X ) -> X = dom f )
107 106 adantr 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> X = dom f )
108 105 107 eleqtrd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> i e. dom f )
109 fvco 
 |-  ( ( Fun f /\ i e. dom f ) -> ( ( abs o. f ) ` i ) = ( abs ` ( f ` i ) ) )
110 104 108 109 syl2an2r 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( ( abs o. f ) ` i ) = ( abs ` ( f ` i ) ) )
111 absfun 
 |-  Fun abs
112 funco 
 |-  ( ( Fun abs /\ Fun f ) -> Fun ( abs o. f ) )
113 111 104 112 sylancr 
 |-  ( f e. ( RR ^m X ) -> Fun ( abs o. f ) )
114 87 64 eleqtrdi 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( f ` i ) e. dom abs )
115 dmfco 
 |-  ( ( Fun f /\ i e. dom f ) -> ( i e. dom ( abs o. f ) <-> ( f ` i ) e. dom abs ) )
116 104 108 115 syl2an2r 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( i e. dom ( abs o. f ) <-> ( f ` i ) e. dom abs ) )
117 114 116 mpbird 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> i e. dom ( abs o. f ) )
118 fvelrn 
 |-  ( ( Fun ( abs o. f ) /\ i e. dom ( abs o. f ) ) -> ( ( abs o. f ) ` i ) e. ran ( abs o. f ) )
119 113 117 118 syl2an2r 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( ( abs o. f ) ` i ) e. ran ( abs o. f ) )
120 110 119 eqeltrrd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. ran ( abs o. f ) )
121 120 adantll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. ran ( abs o. f ) )
122 121 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. ran ( abs o. f ) )
123 97 99 103 122 suprubd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( abs ` ( f ` i ) ) <_ sup ( ran ( abs o. f ) , RR , < ) )
124 45 90 85 96 123 letrd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u ( f ` i ) <_ sup ( ran ( abs o. f ) , RR , < ) )
125 simpl3 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> sup ( ran ( abs o. f ) , RR , < ) < j )
126 45 85 41 124 125 lelttrd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u ( f ` i ) < j )
127 44 41 126 ltnegcon1d 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j < ( f ` i ) )
128 42 44 127 ltled 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j <_ ( f ` i ) )
129 44 leabsd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) <_ ( abs ` ( f ` i ) ) )
130 44 90 85 129 123 letrd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) <_ sup ( ran ( abs o. f ) , RR , < ) )
131 44 85 41 130 125 lelttrd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) < j )
132 31 34 38 128 131 elicod 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. ( -u j [,) j ) )
133 24 25 26 27 132 syl31anc 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. ( -u j [,) j ) )
134 133 adantl3r 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. ( -u j [,) j ) )
135 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
136 fconstmpt 
 |-  ( X X. { <. -u j , j >. } ) = ( x e. X |-> <. -u j , j >. )
137 snex 
 |-  { <. -u j , j >. } e. _V
138 137 a1i 
 |-  ( ph -> { <. -u j , j >. } e. _V )
139 2 138 xpexd 
 |-  ( ph -> ( X X. { <. -u j , j >. } ) e. _V )
140 136 139 eqeltrrid 
 |-  ( ph -> ( x e. X |-> <. -u j , j >. ) e. _V )
141 140 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( x e. X |-> <. -u j , j >. ) e. _V )
142 1 fvmpt2 
 |-  ( ( j e. NN /\ ( x e. X |-> <. -u j , j >. ) e. _V ) -> ( I ` j ) = ( x e. X |-> <. -u j , j >. ) )
143 135 141 142 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) = ( x e. X |-> <. -u j , j >. ) )
144 143 fveq1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( I ` j ) ` i ) = ( ( x e. X |-> <. -u j , j >. ) ` i ) )
145 144 3adant3 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( ( I ` j ) ` i ) = ( ( x e. X |-> <. -u j , j >. ) ` i ) )
146 eqidd 
 |-  ( i e. X -> ( x e. X |-> <. -u j , j >. ) = ( x e. X |-> <. -u j , j >. ) )
147 eqidd 
 |-  ( ( i e. X /\ x = i ) -> <. -u j , j >. = <. -u j , j >. )
148 id 
 |-  ( i e. X -> i e. X )
149 opex 
 |-  <. -u j , j >. e. _V
150 149 a1i 
 |-  ( i e. X -> <. -u j , j >. e. _V )
151 146 147 148 150 fvmptd 
 |-  ( i e. X -> ( ( x e. X |-> <. -u j , j >. ) ` i ) = <. -u j , j >. )
152 151 3ad2ant3 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( ( x e. X |-> <. -u j , j >. ) ` i ) = <. -u j , j >. )
153 145 152 eqtrd 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( ( I ` j ) ` i ) = <. -u j , j >. )
154 153 fveq2d 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 1st ` ( ( I ` j ) ` i ) ) = ( 1st ` <. -u j , j >. ) )
155 negex 
 |-  -u j e. _V
156 vex 
 |-  j e. _V
157 155 156 op1st 
 |-  ( 1st ` <. -u j , j >. ) = -u j
158 154 157 eqtrdi 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 1st ` ( ( I ` j ) ` i ) ) = -u j )
159 153 fveq2d 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 2nd ` ( ( I ` j ) ` i ) ) = ( 2nd ` <. -u j , j >. ) )
160 155 156 op2nd 
 |-  ( 2nd ` <. -u j , j >. ) = j
161 159 160 eqtrdi 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 2nd ` ( ( I ` j ) ` i ) ) = j )
162 158 161 oveq12d 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) = ( -u j [,) j ) )
163 162 eqcomd 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( -u j [,) j ) = ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) )
164 163 3adant1r 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ i e. X ) -> ( -u j [,) j ) = ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) )
165 164 ad5ant135 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( -u j [,) j ) = ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) )
166 134 165 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) )
167 28 zred 
 |-  ( j e. NN -> -u j e. RR )
168 167 39 opelxpd 
 |-  ( j e. NN -> <. -u j , j >. e. ( RR X. RR ) )
169 168 ad2antlr 
 |-  ( ( ( ph /\ j e. NN ) /\ x e. X ) -> <. -u j , j >. e. ( RR X. RR ) )
170 143 169 fmpt3d 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) : X --> ( RR X. RR ) )
171 170 ad4ant14 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) -> ( I ` j ) : X --> ( RR X. RR ) )
172 171 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( I ` j ) : X --> ( RR X. RR ) )
173 simpr 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> i e. X )
174 172 173 fvovco 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( ( [,) o. ( I ` j ) ) ` i ) = ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) )
175 166 174 eleqtrrd 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. ( ( [,) o. ( I ` j ) ) ` i ) )
176 175 ralrimiva 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> A. i e. X ( f ` i ) e. ( ( [,) o. ( I ` j ) ) ` i ) )
177 vex 
 |-  f e. _V
178 177 elixp 
 |-  ( f e. X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) <-> ( f Fn X /\ A. i e. X ( f ` i ) e. ( ( [,) o. ( I ` j ) ) ` i ) ) )
179 23 176 178 sylanbrc 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f e. X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
180 83 archd 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> E. j e. NN sup ( ran ( abs o. f ) , RR , < ) < j )
181 179 180 reximddv3 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> E. j e. NN f e. X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
182 181 an32s 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. ( RR ^m X ) ) -> E. j e. NN f e. X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
183 182 eliund 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. ( RR ^m X ) ) -> f e. U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
184 183 ssd 
 |-  ( ( ph /\ -. X = (/) ) -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
185 19 184 pm2.61dan 
 |-  ( ph -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )