Metamath Proof Explorer


Theorem ioorrnopnlem

Description: The a point in an indexed product of open intervals is contained in an open ball that is contained in the indexed product of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses ioorrnopnlem.x φ X Fin
ioorrnopnlem.n φ X
ioorrnopnlem.a φ A : X
ioorrnopnlem.b φ B : X
ioorrnopnlem.f φ F i X A i B i
ioorrnopnlem.h H = ran i X if B i F i F i A i B i F i F i A i
ioorrnopnlem.e E = sup H <
ioorrnopnlem.v V = F ball D E
ioorrnopnlem.d D = f X , g X k X f k g k 2
Assertion ioorrnopnlem φ v TopOpen X F v v i X A i B i

Proof

Step Hyp Ref Expression
1 ioorrnopnlem.x φ X Fin
2 ioorrnopnlem.n φ X
3 ioorrnopnlem.a φ A : X
4 ioorrnopnlem.b φ B : X
5 ioorrnopnlem.f φ F i X A i B i
6 ioorrnopnlem.h H = ran i X if B i F i F i A i B i F i F i A i
7 ioorrnopnlem.e E = sup H <
8 ioorrnopnlem.v V = F ball D E
9 ioorrnopnlem.d D = f X , g X k X f k g k 2
10 1 9 rrndsxmet φ D ∞Met X
11 nfv i φ
12 reex V
13 12 a1i φ V
14 ioossre A i B i
15 14 a1i φ i X A i B i
16 11 13 15 ixpssmapc φ i X A i B i X
17 16 5 sseldd φ F X
18 6 a1i φ H = ran i X if B i F i F i A i B i F i F i A i
19 4 ffvelrnda φ i X B i
20 5 adantr φ i X F i X A i B i
21 simpr φ i X i X
22 fvixp2 F i X A i B i i X F i A i B i
23 20 21 22 syl2anc φ i X F i A i B i
24 14 23 sseldi φ i X F i
25 19 24 resubcld φ i X B i F i
26 3 ffvelrnda φ i X A i
27 26 rexrd φ i X A i *
28 19 rexrd φ i X B i *
29 iooltub A i * B i * F i A i B i F i < B i
30 27 28 23 29 syl3anc φ i X F i < B i
31 24 19 posdifd φ i X F i < B i 0 < B i F i
32 30 31 mpbid φ i X 0 < B i F i
33 25 32 elrpd φ i X B i F i +
34 24 26 resubcld φ i X F i A i
35 ioogtlb A i * B i * F i A i B i A i < F i
36 27 28 23 35 syl3anc φ i X A i < F i
37 26 24 posdifd φ i X A i < F i 0 < F i A i
38 36 37 mpbid φ i X 0 < F i A i
39 34 38 elrpd φ i X F i A i +
40 33 39 ifcld φ i X if B i F i F i A i B i F i F i A i +
41 40 ralrimiva φ i X if B i F i F i A i B i F i F i A i +
42 eqid i X if B i F i F i A i B i F i F i A i = i X if B i F i F i A i B i F i F i A i
43 42 rnmptss i X if B i F i F i A i B i F i F i A i + ran i X if B i F i F i A i B i F i F i A i +
44 41 43 syl φ ran i X if B i F i F i A i B i F i F i A i +
45 18 44 eqsstrd φ H +
46 ltso < Or
47 46 a1i φ < Or
48 42 rnmptfi X Fin ran i X if B i F i F i A i B i F i F i A i Fin
49 1 48 syl φ ran i X if B i F i F i A i B i F i F i A i Fin
50 6 49 eqeltrid φ H Fin
51 11 40 42 2 rnmptn0 φ ran i X if B i F i F i A i B i F i F i A i
52 18 51 eqnetrd φ H
53 rpssre +
54 53 a1i φ +
55 45 54 sstrd φ H
56 fiinfcl < Or H Fin H H sup H < H
57 47 50 52 55 56 syl13anc φ sup H < H
58 45 57 sseldd φ sup H < +
59 7 58 eqeltrid φ E +
60 rpxr E + E *
61 59 60 syl φ E *
62 eqid MetOpen D = MetOpen D
63 62 blopn D ∞Met X F X E * F ball D E MetOpen D
64 10 17 61 63 syl3anc φ F ball D E MetOpen D
65 8 a1i φ V = F ball D E
66 1 rrxtopnfi φ TopOpen X = MetOpen f X , g X k X f k g k 2
67 9 eqcomi f X , g X k X f k g k 2 = D
68 67 a1i φ f X , g X k X f k g k 2 = D
69 68 fveq2d φ MetOpen f X , g X k X f k g k 2 = MetOpen D
70 66 69 eqtrd φ TopOpen X = MetOpen D
71 65 70 eleq12d φ V TopOpen X F ball D E MetOpen D
72 64 71 mpbird φ V TopOpen X
73 xmetpsmet D ∞Met X D PsMet X
74 10 73 syl φ D PsMet X
75 blcntrps D PsMet X F X E + F F ball D E
76 74 17 59 75 syl3anc φ F F ball D E
77 65 eqcomd φ F ball D E = V
78 76 77 eleqtrd φ F V
79 nfv g φ
80 elmapfn g X g Fn X
81 80 3ad2ant2 φ g X F D g < E g Fn X
82 27 3ad2antl1 φ g X F D g < E i X A i *
83 28 3ad2antl1 φ g X F D g < E i X B i *
84 simpl2 φ g X F D g < E i X g X
85 simpr φ g X F D g < E i X i X
86 elmapi g X g : X
87 86 adantr g X i X g : X
88 simpr g X i X i X
89 87 88 ffvelrnd g X i X g i
90 84 85 89 syl2anc φ g X F D g < E i X g i
91 26 3ad2antl1 φ g X F D g < E i X A i
92 53 59 sseldi φ E
93 92 adantr φ i X E
94 24 93 resubcld φ i X F i E
95 94 3ad2antl1 φ g X F D g < E i X F i E
96 53 40 sseldi φ i X if B i F i F i A i B i F i F i A i
97 7 a1i φ E = sup H <
98 infxrrefi H H Fin H sup H * < = sup H <
99 55 50 52 98 syl3anc φ sup H * < = sup H <
100 99 eqcomd φ sup H < = sup H * <
101 97 100 eqtrd φ E = sup H * <
102 101 adantr φ i X E = sup H * <
103 ressxr *
104 103 a1i φ *
105 55 104 sstrd φ H *
106 105 adantr φ i X H *
107 40 elexd φ i X if B i F i F i A i B i F i F i A i V
108 42 elrnmpt1 i X if B i F i F i A i B i F i F i A i V if B i F i F i A i B i F i F i A i ran i X if B i F i F i A i B i F i F i A i
109 21 107 108 syl2anc φ i X if B i F i F i A i B i F i F i A i ran i X if B i F i F i A i B i F i F i A i
110 109 6 eleqtrrdi φ i X if B i F i F i A i B i F i F i A i H
111 infxrlb H * if B i F i F i A i B i F i F i A i H sup H * < if B i F i F i A i B i F i F i A i
112 106 110 111 syl2anc φ i X sup H * < if B i F i F i A i B i F i F i A i
113 102 112 eqbrtrd φ i X E if B i F i F i A i B i F i F i A i
114 min2 B i F i F i A i if B i F i F i A i B i F i F i A i F i A i
115 25 34 114 syl2anc φ i X if B i F i F i A i B i F i F i A i F i A i
116 93 96 34 113 115 letrd φ i X E F i A i
117 93 24 26 116 lesubd φ i X A i F i E
118 117 3ad2antl1 φ g X F D g < E i X A i F i E
119 24 adantlr φ g X i X F i
120 89 adantll φ g X i X g i
121 119 120 resubcld φ g X i X F i g i
122 121 3adantl3 φ g X F D g < E i X F i g i
123 1 9 rrndsmet φ D Met X
124 123 ad2antrr φ g X i X D Met X
125 17 ad2antrr φ g X i X F X
126 simplr φ g X i X g X
127 metcl D Met X F X g X F D g
128 124 125 126 127 syl3anc φ g X i X F D g
129 128 3adantl3 φ g X F D g < E i X F D g
130 93 adantlr φ g X i X E
131 130 3adantl3 φ g X F D g < E i X E
132 121 recnd φ g X i X F i g i
133 132 abscld φ g X i X F i g i
134 121 leabsd φ g X i X F i g i F i g i
135 1 ad2antrr φ g X i X X Fin
136 ixpf F i X A i B i F : X i X A i B i
137 5 136 syl φ F : X i X A i B i
138 15 ralrimiva φ i X A i B i
139 iunss i X A i B i i X A i B i
140 138 139 sylibr φ i X A i B i
141 137 140 fssd φ F : X
142 141 ad2antrr φ g X i X F : X
143 126 86 syl φ g X i X g : X
144 simpr φ g X i X i X
145 eqid dist X = dist X
146 135 142 143 144 145 rrnprjdstle φ g X i X F i g i F dist X g
147 eqid X = X
148 eqid X = X
149 147 148 rrxdsfi X Fin dist X = f X , g X k X f k g k 2
150 1 149 syl φ dist X = f X , g X k X f k g k 2
151 150 68 eqtrd φ dist X = D
152 151 oveqd φ F dist X g = F D g
153 152 ad2antrr φ g X i X F dist X g = F D g
154 146 153 breqtrd φ g X i X F i g i F D g
155 121 133 128 134 154 letrd φ g X i X F i g i F D g
156 155 3adantl3 φ g X F D g < E i X F i g i F D g
157 simpl3 φ g X F D g < E i X F D g < E
158 122 129 131 156 157 lelttrd φ g X F D g < E i X F i g i < E
159 ltsub23 F i g i E F i g i < E F i E < g i
160 119 120 130 159 syl3anc φ g X i X F i g i < E F i E < g i
161 160 3adantl3 φ g X F D g < E i X F i g i < E F i E < g i
162 158 161 mpbid φ g X F D g < E i X F i E < g i
163 91 95 90 118 162 lelttrd φ g X F D g < E i X A i < g i
164 24 93 readdcld φ i X F i + E
165 164 3ad2antl1 φ g X F D g < E i X F i + E
166 19 3ad2antl1 φ g X F D g < E i X B i
167 120 119 resubcld φ g X i X g i F i
168 167 3adantl3 φ g X F D g < E i X g i F i
169 167 leabsd φ g X i X g i F i g i F i
170 120 recnd φ g X i X g i
171 119 recnd φ g X i X F i
172 170 171 abssubd φ g X i X g i F i = F i g i
173 169 172 breqtrd φ g X i X g i F i F i g i
174 167 133 128 173 154 letrd φ g X i X g i F i F D g
175 174 3adantl3 φ g X F D g < E i X g i F i F D g
176 168 129 131 175 157 lelttrd φ g X F D g < E i X g i F i < E
177 119 3adantl3 φ g X F D g < E i X F i
178 90 177 131 ltsubadd2d φ g X F D g < E i X g i F i < E g i < F i + E
179 176 178 mpbid φ g X F D g < E i X g i < F i + E
180 min1 B i F i F i A i if B i F i F i A i B i F i F i A i B i F i
181 25 34 180 syl2anc φ i X if B i F i F i A i B i F i F i A i B i F i
182 93 96 25 113 181 letrd φ i X E B i F i
183 24 93 19 leaddsub2d φ i X F i + E B i E B i F i
184 182 183 mpbird φ i X F i + E B i
185 184 3ad2antl1 φ g X F D g < E i X F i + E B i
186 90 165 166 179 185 ltletrd φ g X F D g < E i X g i < B i
187 82 83 90 163 186 eliood φ g X F D g < E i X g i A i B i
188 187 ralrimiva φ g X F D g < E i X g i A i B i
189 81 188 jca φ g X F D g < E g Fn X i X g i A i B i
190 vex g V
191 190 elixp g i X A i B i g Fn X i X g i A i B i
192 189 191 sylibr φ g X F D g < E g i X A i B i
193 79 74 17 61 192 ballss3 φ F ball D E i X A i B i
194 65 193 eqsstrd φ V i X A i B i
195 78 194 jca φ F V V i X A i B i
196 eleq2 v = V F v F V
197 sseq1 v = V v i X A i B i V i X A i B i
198 196 197 anbi12d v = V F v v i X A i B i F V V i X A i B i
199 198 rspcev V TopOpen X F V V i X A i B i v TopOpen X F v v i X A i B i
200 72 195 199 syl2anc φ v TopOpen X F v v i X A i B i