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)

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 5 a1i 
 |-  ( X = (/) -> ( RR ^m (/) ) = { (/) } )
7 oveq2 
 |-  ( X = (/) -> ( RR ^m X ) = ( RR ^m (/) ) )
8 ixpeq1 
 |-  ( X = (/) -> X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) = X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) )
9 8 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 ) )
10 ixp0x 
 |-  X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = { (/) }
11 10 a1i 
 |-  ( j e. NN -> X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = { (/) } )
12 11 iuneq2i 
 |-  U_ j e. NN X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = U_ j e. NN { (/) }
13 1nn 
 |-  1 e. NN
14 13 ne0ii 
 |-  NN =/= (/)
15 iunconst 
 |-  ( NN =/= (/) -> U_ j e. NN { (/) } = { (/) } )
16 14 15 ax-mp 
 |-  U_ j e. NN { (/) } = { (/) }
17 12 16 eqtri 
 |-  U_ j e. NN X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = { (/) }
18 17 a1i 
 |-  ( X = (/) -> U_ j e. NN X_ i e. (/) ( ( [,) o. ( I ` j ) ) ` i ) = { (/) } )
19 9 18 eqtrd 
 |-  ( X = (/) -> U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) = { (/) } )
20 6 7 19 3eqtr4d 
 |-  ( X = (/) -> ( RR ^m X ) = U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
21 eqimss 
 |-  ( ( RR ^m X ) = U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
22 20 21 syl 
 |-  ( X = (/) -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
23 22 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
24 simpll 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. ( RR ^m X ) ) -> ph )
25 simpr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. ( RR ^m X ) ) -> f e. ( RR ^m X ) )
26 simplr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. ( RR ^m X ) ) -> -. X = (/) )
27 rncoss 
 |-  ran ( abs o. f ) C_ ran abs
28 absf 
 |-  abs : CC --> RR
29 frn 
 |-  ( abs : CC --> RR -> ran abs C_ RR )
30 28 29 ax-mp 
 |-  ran abs C_ RR
31 27 30 sstri 
 |-  ran ( abs o. f ) C_ RR
32 31 a1i 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> ran ( abs o. f ) C_ RR )
33 ltso 
 |-  < Or RR
34 33 a1i 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> < Or RR )
35 28 a1i 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> abs : CC --> RR )
36 elmapi 
 |-  ( f e. ( RR ^m X ) -> f : X --> RR )
37 36 adantl 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f : X --> RR )
38 ax-resscn 
 |-  RR C_ CC
39 38 a1i 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> RR C_ CC )
40 37 39 fssd 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f : X --> CC )
41 fco 
 |-  ( ( abs : CC --> RR /\ f : X --> CC ) -> ( abs o. f ) : X --> RR )
42 35 40 41 syl2anc 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> ( abs o. f ) : X --> RR )
43 2 adantr 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> X e. Fin )
44 rnffi 
 |-  ( ( ( abs o. f ) : X --> RR /\ X e. Fin ) -> ran ( abs o. f ) e. Fin )
45 42 43 44 syl2anc 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> ran ( abs o. f ) e. Fin )
46 45 adantr 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> ran ( abs o. f ) e. Fin )
47 36 frnd 
 |-  ( f e. ( RR ^m X ) -> ran f C_ RR )
48 28 fdmi 
 |-  dom abs = CC
49 48 eqcomi 
 |-  CC = dom abs
50 38 49 sseqtri 
 |-  RR C_ dom abs
51 50 a1i 
 |-  ( f e. ( RR ^m X ) -> RR C_ dom abs )
52 47 51 sstrd 
 |-  ( f e. ( RR ^m X ) -> ran f C_ dom abs )
53 dmcosseq 
 |-  ( ran f C_ dom abs -> dom ( abs o. f ) = dom f )
54 52 53 syl 
 |-  ( f e. ( RR ^m X ) -> dom ( abs o. f ) = dom f )
55 36 fdmd 
 |-  ( f e. ( RR ^m X ) -> dom f = X )
56 54 55 eqtrd 
 |-  ( f e. ( RR ^m X ) -> dom ( abs o. f ) = X )
57 56 adantr 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> dom ( abs o. f ) = X )
58 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
59 58 adantl 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> X =/= (/) )
60 57 59 eqnetrd 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> dom ( abs o. f ) =/= (/) )
61 60 neneqd 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> -. dom ( abs o. f ) = (/) )
62 dm0rn0 
 |-  ( dom ( abs o. f ) = (/) <-> ran ( abs o. f ) = (/) )
63 61 62 sylnib 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> -. ran ( abs o. f ) = (/) )
64 63 neqned 
 |-  ( ( f e. ( RR ^m X ) /\ -. X = (/) ) -> ran ( abs o. f ) =/= (/) )
65 64 adantll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> ran ( abs o. f ) =/= (/) )
66 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 ) )
67 34 46 65 32 66 syl13anc 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> sup ( ran ( abs o. f ) , RR , < ) e. ran ( abs o. f ) )
68 32 67 sseldd 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> sup ( ran ( abs o. f ) , RR , < ) e. RR )
69 arch 
 |-  ( sup ( ran ( abs o. f ) , RR , < ) e. RR -> E. j e. NN sup ( ran ( abs o. f ) , RR , < ) < j )
70 68 69 syl 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> E. j e. NN sup ( ran ( abs o. f ) , RR , < ) < j )
71 37 ffnd 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> f Fn X )
72 71 ad2antrr 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f Fn X )
73 72 adantlr 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f Fn X )
74 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 ) ) )
75 id 
 |-  ( j e. NN -> j e. NN )
76 75 ad3antlr 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> j e. NN )
77 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 )
78 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> i e. X )
79 simp2 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> j e. NN )
80 zssre 
 |-  ZZ C_ RR
81 ressxr 
 |-  RR C_ RR*
82 80 81 sstri 
 |-  ZZ C_ RR*
83 nnnegz 
 |-  ( j e. NN -> -u j e. ZZ )
84 82 83 sselid 
 |-  ( j e. NN -> -u j e. RR* )
85 84 adantr 
 |-  ( ( j e. NN /\ i e. X ) -> -u j e. RR* )
86 79 85 sylan 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j e. RR* )
87 75 nnxrd 
 |-  ( j e. NN -> j e. RR* )
88 87 adantr 
 |-  ( ( j e. NN /\ i e. X ) -> j e. RR* )
89 79 88 sylan 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> j e. RR* )
90 36 3ad2ant1 
 |-  ( ( f e. ( RR ^m X ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f : X --> RR )
91 81 a1i 
 |-  ( ( f e. ( RR ^m X ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> RR C_ RR* )
92 90 91 fssd 
 |-  ( ( f e. ( RR ^m X ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f : X --> RR* )
93 92 3adant1l 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> f : X --> RR* )
94 93 ffvelcdmda 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. RR* )
95 nnre 
 |-  ( j e. NN -> j e. RR )
96 95 adantr 
 |-  ( ( j e. NN /\ i e. X ) -> j e. RR )
97 96 3ad2antl2 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> j e. RR )
98 97 renegcld 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j e. RR )
99 37 ffvelcdmda 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ( f ` i ) e. RR )
100 99 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. RR )
101 100 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 )
102 simpll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ph )
103 simplr 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> f e. ( RR ^m X ) )
104 n0i 
 |-  ( i e. X -> -. X = (/) )
105 104 adantl 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> -. X = (/) )
106 102 103 105 68 syl21anc 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> sup ( ran ( abs o. f ) , RR , < ) e. RR )
107 106 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 )
108 36 ffvelcdmda 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( f ` i ) e. RR )
109 38 108 sselid 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( f ` i ) e. CC )
110 109 abscld 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. RR )
111 110 adantll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. RR )
112 111 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 )
113 108 renegcld 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> -u ( f ` i ) e. RR )
114 113 leabsd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> -u ( f ` i ) <_ ( abs ` -u ( f ` i ) ) )
115 109 absnegd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( abs ` -u ( f ` i ) ) = ( abs ` ( f ` i ) ) )
116 114 115 breqtrd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> -u ( f ` i ) <_ ( abs ` ( f ` i ) ) )
117 116 adantll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> -u ( f ` i ) <_ ( abs ` ( f ` i ) ) )
118 117 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 ) ) )
119 31 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 )
120 105 65 syldan 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ran ( abs o. f ) =/= (/) )
121 120 3ad2antl1 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ran ( abs o. f ) =/= (/) )
122 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 )
123 31 45 122 sylancr 
 |-  ( ( ph /\ f e. ( RR ^m X ) ) -> E. y e. RR A. z e. ran ( abs o. f ) z <_ y )
124 123 adantr 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> E. y e. RR A. z e. ran ( abs o. f ) z <_ y )
125 124 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 )
126 elmapfun 
 |-  ( f e. ( RR ^m X ) -> Fun f )
127 126 adantr 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> Fun f )
128 simpr 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> i e. X )
129 55 eqcomd 
 |-  ( f e. ( RR ^m X ) -> X = dom f )
130 129 adantr 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> X = dom f )
131 128 130 eleqtrd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> i e. dom f )
132 fvco 
 |-  ( ( Fun f /\ i e. dom f ) -> ( ( abs o. f ) ` i ) = ( abs ` ( f ` i ) ) )
133 127 131 132 syl2anc 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( ( abs o. f ) ` i ) = ( abs ` ( f ` i ) ) )
134 133 eqcomd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( abs ` ( f ` i ) ) = ( ( abs o. f ) ` i ) )
135 absfun 
 |-  Fun abs
136 135 a1i 
 |-  ( f e. ( RR ^m X ) -> Fun abs )
137 funco 
 |-  ( ( Fun abs /\ Fun f ) -> Fun ( abs o. f ) )
138 136 126 137 syl2anc 
 |-  ( f e. ( RR ^m X ) -> Fun ( abs o. f ) )
139 138 adantr 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> Fun ( abs o. f ) )
140 109 49 eleqtrdi 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( f ` i ) e. dom abs )
141 dmfco 
 |-  ( ( Fun f /\ i e. dom f ) -> ( i e. dom ( abs o. f ) <-> ( f ` i ) e. dom abs ) )
142 127 131 141 syl2anc 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( i e. dom ( abs o. f ) <-> ( f ` i ) e. dom abs ) )
143 140 142 mpbird 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> i e. dom ( abs o. f ) )
144 fvelrn 
 |-  ( ( Fun ( abs o. f ) /\ i e. dom ( abs o. f ) ) -> ( ( abs o. f ) ` i ) e. ran ( abs o. f ) )
145 139 143 144 syl2anc 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( ( abs o. f ) ` i ) e. ran ( abs o. f ) )
146 134 145 eqeltrd 
 |-  ( ( f e. ( RR ^m X ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. ran ( abs o. f ) )
147 146 adantll 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ i e. X ) -> ( abs ` ( f ` i ) ) e. ran ( abs o. f ) )
148 147 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 ) )
149 suprub 
 |-  ( ( ( ran ( abs o. f ) C_ RR /\ ran ( abs o. f ) =/= (/) /\ E. y e. RR A. z e. ran ( abs o. f ) z <_ y ) /\ ( abs ` ( f ` i ) ) e. ran ( abs o. f ) ) -> ( abs ` ( f ` i ) ) <_ sup ( ran ( abs o. f ) , RR , < ) )
150 119 121 125 148 149 syl31anc 
 |-  ( ( ( ( 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 , < ) )
151 101 112 107 118 150 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 , < ) )
152 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 )
153 101 107 97 151 152 lelttrd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u ( f ` i ) < j )
154 101 97 ltnegd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( -u ( f ` i ) < j <-> -u j < -u -u ( f ` i ) ) )
155 153 154 mpbid 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j < -u -u ( f ` i ) )
156 38 100 sselid 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) e. CC )
157 156 negnegd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u -u ( f ` i ) = ( f ` i ) )
158 155 157 breqtrd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j < ( f ` i ) )
159 98 100 158 ltled 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> -u j <_ ( f ` i ) )
160 100 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 ) ) )
161 100 112 107 160 150 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 , < ) )
162 100 107 97 161 152 lelttrd 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( f ` i ) < j )
163 86 89 94 159 162 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 ) )
164 74 76 77 78 163 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 ) )
165 164 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 ) )
166 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
167 mptexg 
 |-  ( X e. Fin -> ( x e. X |-> <. -u j , j >. ) e. _V )
168 2 167 syl 
 |-  ( ph -> ( x e. X |-> <. -u j , j >. ) e. _V )
169 168 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( x e. X |-> <. -u j , j >. ) e. _V )
170 1 fvmpt2 
 |-  ( ( j e. NN /\ ( x e. X |-> <. -u j , j >. ) e. _V ) -> ( I ` j ) = ( x e. X |-> <. -u j , j >. ) )
171 166 169 170 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) = ( x e. X |-> <. -u j , j >. ) )
172 171 fveq1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( I ` j ) ` i ) = ( ( x e. X |-> <. -u j , j >. ) ` i ) )
173 172 3adant3 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( ( I ` j ) ` i ) = ( ( x e. X |-> <. -u j , j >. ) ` i ) )
174 eqidd 
 |-  ( i e. X -> ( x e. X |-> <. -u j , j >. ) = ( x e. X |-> <. -u j , j >. ) )
175 eqid 
 |-  <. -u j , j >. = <. -u j , j >.
176 175 a1i 
 |-  ( ( i e. X /\ x = i ) -> <. -u j , j >. = <. -u j , j >. )
177 id 
 |-  ( i e. X -> i e. X )
178 opex 
 |-  <. -u j , j >. e. _V
179 178 a1i 
 |-  ( i e. X -> <. -u j , j >. e. _V )
180 174 176 177 179 fvmptd 
 |-  ( i e. X -> ( ( x e. X |-> <. -u j , j >. ) ` i ) = <. -u j , j >. )
181 180 3ad2ant3 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( ( x e. X |-> <. -u j , j >. ) ` i ) = <. -u j , j >. )
182 173 181 eqtrd 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( ( I ` j ) ` i ) = <. -u j , j >. )
183 182 fveq2d 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 1st ` ( ( I ` j ) ` i ) ) = ( 1st ` <. -u j , j >. ) )
184 negex 
 |-  -u j e. _V
185 vex 
 |-  j e. _V
186 184 185 op1st 
 |-  ( 1st ` <. -u j , j >. ) = -u j
187 186 a1i 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 1st ` <. -u j , j >. ) = -u j )
188 183 187 eqtrd 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 1st ` ( ( I ` j ) ` i ) ) = -u j )
189 182 fveq2d 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 2nd ` ( ( I ` j ) ` i ) ) = ( 2nd ` <. -u j , j >. ) )
190 184 185 op2nd 
 |-  ( 2nd ` <. -u j , j >. ) = j
191 190 a1i 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 2nd ` <. -u j , j >. ) = j )
192 189 191 eqtrd 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( 2nd ` ( ( I ` j ) ` i ) ) = j )
193 188 192 oveq12d 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) = ( -u j [,) j ) )
194 193 eqcomd 
 |-  ( ( ph /\ j e. NN /\ i e. X ) -> ( -u j [,) j ) = ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) )
195 194 3adant1r 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ j e. NN /\ i e. X ) -> ( -u j [,) j ) = ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) )
196 195 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 ) ) ) )
197 165 196 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 ) ) ) )
198 80 83 sselid 
 |-  ( j e. NN -> -u j e. RR )
199 opelxpi 
 |-  ( ( -u j e. RR /\ j e. RR ) -> <. -u j , j >. e. ( RR X. RR ) )
200 198 95 199 syl2anc 
 |-  ( j e. NN -> <. -u j , j >. e. ( RR X. RR ) )
201 200 ad2antlr 
 |-  ( ( ( ph /\ j e. NN ) /\ x e. X ) -> <. -u j , j >. e. ( RR X. RR ) )
202 eqid 
 |-  ( x e. X |-> <. -u j , j >. ) = ( x e. X |-> <. -u j , j >. )
203 201 202 fmptd 
 |-  ( ( ph /\ j e. NN ) -> ( x e. X |-> <. -u j , j >. ) : X --> ( RR X. RR ) )
204 171 feq1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( I ` j ) : X --> ( RR X. RR ) <-> ( x e. X |-> <. -u j , j >. ) : X --> ( RR X. RR ) ) )
205 203 204 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) : X --> ( RR X. RR ) )
206 205 ad4ant14 
 |-  ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) -> ( I ` j ) : X --> ( RR X. RR ) )
207 206 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 ) )
208 simpr 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> i e. X )
209 207 208 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 ) ) ) )
210 209 eqcomd 
 |-  ( ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) /\ i e. X ) -> ( ( 1st ` ( ( I ` j ) ` i ) ) [,) ( 2nd ` ( ( I ` j ) ` i ) ) ) = ( ( [,) o. ( I ` j ) ) ` i ) )
211 197 210 eleqtrd 
 |-  ( ( ( ( ( ( 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 ) )
212 211 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 ) )
213 73 212 jca 
 |-  ( ( ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) /\ j e. NN ) /\ sup ( ran ( abs o. f ) , RR , < ) < j ) -> ( f Fn X /\ A. i e. X ( f ` i ) e. ( ( [,) o. ( I ` j ) ) ` i ) ) )
214 vex 
 |-  f e. _V
215 214 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 ) ) )
216 213 215 sylibr 
 |-  ( ( ( ( ( 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 ) )
217 216 ex 
 |-  ( ( ( ( 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 ) ) )
218 217 reximdva 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> ( E. j e. NN sup ( ran ( abs o. f ) , RR , < ) < j -> E. j e. NN f e. X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) ) )
219 70 218 mpd 
 |-  ( ( ( ph /\ f e. ( RR ^m X ) ) /\ -. X = (/) ) -> E. j e. NN f e. X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
220 24 25 26 219 syl21anc 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. ( RR ^m X ) ) -> E. j e. NN f e. X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
221 eliun 
 |-  ( f e. U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) <-> E. j e. NN f e. X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
222 220 221 sylibr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ f e. ( RR ^m X ) ) -> f e. U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
223 222 ralrimiva 
 |-  ( ( ph /\ -. X = (/) ) -> A. f e. ( RR ^m X ) f e. U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
224 dfss3 
 |-  ( ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) <-> A. f e. ( RR ^m X ) f e. U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
225 223 224 sylibr 
 |-  ( ( ph /\ -. X = (/) ) -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )
226 23 225 pm2.61dan 
 |-  ( ph -> ( RR ^m X ) C_ U_ j e. NN X_ i e. X ( ( [,) o. ( I ` j ) ) ` i ) )