Metamath Proof Explorer


Theorem prdsxmslem2

Description: Lemma for prdsxms . The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses prdsxms.y Y = S 𝑠 R
prdsxms.s φ S W
prdsxms.i φ I Fin
prdsxms.d D = dist Y
prdsxms.b B = Base Y
prdsxms.r φ R : I ∞MetSp
prdsxms.j J = TopOpen Y
prdsxms.v V = Base R k
prdsxms.e E = dist R k V × V
prdsxms.k K = TopOpen R k
prdsxms.c C = x | g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
Assertion prdsxmslem2 φ J = MetOpen D

Proof

Step Hyp Ref Expression
1 prdsxms.y Y = S 𝑠 R
2 prdsxms.s φ S W
3 prdsxms.i φ I Fin
4 prdsxms.d D = dist Y
5 prdsxms.b B = Base Y
6 prdsxms.r φ R : I ∞MetSp
7 prdsxms.j J = TopOpen Y
8 prdsxms.v V = Base R k
9 prdsxms.e E = dist R k V × V
10 prdsxms.k K = TopOpen R k
11 prdsxms.c C = x | g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
12 topnfn TopOpen Fn V
13 6 ffnd φ R Fn I
14 dffn2 R Fn I R : I V
15 13 14 sylib φ R : I V
16 fnfco TopOpen Fn V R : I V TopOpen R Fn I
17 12 15 16 sylancr φ TopOpen R Fn I
18 11 ptval I Fin TopOpen R Fn I 𝑡 TopOpen R = topGen C
19 3 17 18 syl2anc φ 𝑡 TopOpen R = topGen C
20 eldifsn x ran ball D x ran ball D x
21 1 2 3 4 5 6 prdsxmslem1 φ D ∞Met B
22 blrn D ∞Met B x ran ball D p B r * x = p ball D r
23 21 22 syl φ x ran ball D p B r * x = p ball D r
24 21 adantr φ p B r * D ∞Met B
25 simprl φ p B r * p B
26 simprr φ p B r * r *
27 xbln0 D ∞Met B p B r * p ball D r 0 < r
28 24 25 26 27 syl3anc φ p B r * p ball D r 0 < r
29 3 3ad2ant1 φ p B r * 0 < r I Fin
30 29 mptexd φ p B r * 0 < r n I p n ball dist R n Base R n × Base R n r V
31 ovex p n ball dist R n Base R n × Base R n r V
32 31 rgenw n I p n ball dist R n Base R n × Base R n r V
33 eqid n I p n ball dist R n Base R n × Base R n r = n I p n ball dist R n Base R n × Base R n r
34 33 fnmpt n I p n ball dist R n Base R n × Base R n r V n I p n ball dist R n Base R n × Base R n r Fn I
35 32 34 mp1i φ p B r * 0 < r n I p n ball dist R n Base R n × Base R n r Fn I
36 6 3ad2ant1 φ p B r * 0 < r R : I ∞MetSp
37 36 ffvelrnda φ p B r * 0 < r k I R k ∞MetSp
38 8 9 xmsxmet R k ∞MetSp E ∞Met V
39 37 38 syl φ p B r * 0 < r k I E ∞Met V
40 eqid S 𝑠 k I R k = S 𝑠 k I R k
41 eqid Base S 𝑠 k I R k = Base S 𝑠 k I R k
42 2 3ad2ant1 φ p B r * 0 < r S W
43 37 ralrimiva φ p B r * 0 < r k I R k ∞MetSp
44 simp2l φ p B r * 0 < r p B
45 36 feqmptd φ p B r * 0 < r R = k I R k
46 45 oveq2d φ p B r * 0 < r S 𝑠 R = S 𝑠 k I R k
47 1 46 syl5eq φ p B r * 0 < r Y = S 𝑠 k I R k
48 47 fveq2d φ p B r * 0 < r Base Y = Base S 𝑠 k I R k
49 5 48 syl5eq φ p B r * 0 < r B = Base S 𝑠 k I R k
50 44 49 eleqtrd φ p B r * 0 < r p Base S 𝑠 k I R k
51 40 41 42 29 43 8 50 prdsbascl φ p B r * 0 < r k I p k V
52 51 r19.21bi φ p B r * 0 < r k I p k V
53 simp2r φ p B r * 0 < r r *
54 53 adantr φ p B r * 0 < r k I r *
55 eqid MetOpen E = MetOpen E
56 55 blopn E ∞Met V p k V r * p k ball E r MetOpen E
57 39 52 54 56 syl3anc φ p B r * 0 < r k I p k ball E r MetOpen E
58 2fveq3 n = k dist R n = dist R k
59 2fveq3 n = k Base R n = Base R k
60 59 8 eqtr4di n = k Base R n = V
61 60 sqxpeqd n = k Base R n × Base R n = V × V
62 58 61 reseq12d n = k dist R n Base R n × Base R n = dist R k V × V
63 62 9 eqtr4di n = k dist R n Base R n × Base R n = E
64 63 fveq2d n = k ball dist R n Base R n × Base R n = ball E
65 fveq2 n = k p n = p k
66 eqidd n = k r = r
67 64 65 66 oveq123d n = k p n ball dist R n Base R n × Base R n r = p k ball E r
68 ovex p k ball E r V
69 67 33 68 fvmpt k I n I p n ball dist R n Base R n × Base R n r k = p k ball E r
70 69 adantl φ p B r * 0 < r k I n I p n ball dist R n Base R n × Base R n r k = p k ball E r
71 fvco3 R : I ∞MetSp k I TopOpen R k = TopOpen R k
72 71 10 eqtr4di R : I ∞MetSp k I TopOpen R k = K
73 36 72 sylan φ p B r * 0 < r k I TopOpen R k = K
74 10 8 9 xmstopn R k ∞MetSp K = MetOpen E
75 37 74 syl φ p B r * 0 < r k I K = MetOpen E
76 73 75 eqtrd φ p B r * 0 < r k I TopOpen R k = MetOpen E
77 57 70 76 3eltr4d φ p B r * 0 < r k I n I p n ball dist R n Base R n × Base R n r k TopOpen R k
78 77 ralrimiva φ p B r * 0 < r k I n I p n ball dist R n Base R n × Base R n r k TopOpen R k
79 36 feqmptd φ p B r * 0 < r R = n I R n
80 79 oveq2d φ p B r * 0 < r S 𝑠 R = S 𝑠 n I R n
81 1 80 syl5eq φ p B r * 0 < r Y = S 𝑠 n I R n
82 81 fveq2d φ p B r * 0 < r dist Y = dist S 𝑠 n I R n
83 4 82 syl5eq φ p B r * 0 < r D = dist S 𝑠 n I R n
84 83 fveq2d φ p B r * 0 < r ball D = ball dist S 𝑠 n I R n
85 84 oveqd φ p B r * 0 < r p ball D r = p ball dist S 𝑠 n I R n r
86 fveq2 n = k R n = R k
87 86 cbvmptv n I R n = k I R k
88 87 oveq2i S 𝑠 n I R n = S 𝑠 k I R k
89 eqid Base S 𝑠 n I R n = Base S 𝑠 n I R n
90 eqid dist S 𝑠 n I R n = dist S 𝑠 n I R n
91 81 fveq2d φ p B r * 0 < r Base Y = Base S 𝑠 n I R n
92 5 91 syl5eq φ p B r * 0 < r B = Base S 𝑠 n I R n
93 44 92 eleqtrd φ p B r * 0 < r p Base S 𝑠 n I R n
94 simp3 φ p B r * 0 < r 0 < r
95 88 89 8 9 90 42 29 37 39 93 53 94 prdsbl φ p B r * 0 < r p ball dist S 𝑠 n I R n r = k I p k ball E r
96 85 95 eqtrd φ p B r * 0 < r p ball D r = k I p k ball E r
97 fneq1 g = n I p n ball dist R n Base R n × Base R n r g Fn I n I p n ball dist R n Base R n × Base R n r Fn I
98 fveq1 g = n I p n ball dist R n Base R n × Base R n r g k = n I p n ball dist R n Base R n × Base R n r k
99 98 eleq1d g = n I p n ball dist R n Base R n × Base R n r g k TopOpen R k n I p n ball dist R n Base R n × Base R n r k TopOpen R k
100 99 ralbidv g = n I p n ball dist R n Base R n × Base R n r k I g k TopOpen R k k I n I p n ball dist R n Base R n × Base R n r k TopOpen R k
101 97 100 anbi12d g = n I p n ball dist R n Base R n × Base R n r g Fn I k I g k TopOpen R k n I p n ball dist R n Base R n × Base R n r Fn I k I n I p n ball dist R n Base R n × Base R n r k TopOpen R k
102 98 69 sylan9eq g = n I p n ball dist R n Base R n × Base R n r k I g k = p k ball E r
103 102 ixpeq2dva g = n I p n ball dist R n Base R n × Base R n r k I g k = k I p k ball E r
104 103 eqeq2d g = n I p n ball dist R n Base R n × Base R n r p ball D r = k I g k p ball D r = k I p k ball E r
105 101 104 anbi12d g = n I p n ball dist R n Base R n × Base R n r g Fn I k I g k TopOpen R k p ball D r = k I g k n I p n ball dist R n Base R n × Base R n r Fn I k I n I p n ball dist R n Base R n × Base R n r k TopOpen R k p ball D r = k I p k ball E r
106 105 spcegv n I p n ball dist R n Base R n × Base R n r V n I p n ball dist R n Base R n × Base R n r Fn I k I n I p n ball dist R n Base R n × Base R n r k TopOpen R k p ball D r = k I p k ball E r g g Fn I k I g k TopOpen R k p ball D r = k I g k
107 106 3impib n I p n ball dist R n Base R n × Base R n r V n I p n ball dist R n Base R n × Base R n r Fn I k I n I p n ball dist R n Base R n × Base R n r k TopOpen R k p ball D r = k I p k ball E r g g Fn I k I g k TopOpen R k p ball D r = k I g k
108 30 35 78 96 107 syl121anc φ p B r * 0 < r g g Fn I k I g k TopOpen R k p ball D r = k I g k
109 108 3expia φ p B r * 0 < r g g Fn I k I g k TopOpen R k p ball D r = k I g k
110 28 109 sylbid φ p B r * p ball D r g g Fn I k I g k TopOpen R k p ball D r = k I g k
111 110 adantr φ p B r * x = p ball D r p ball D r g g Fn I k I g k TopOpen R k p ball D r = k I g k
112 simpr φ p B r * x = p ball D r x = p ball D r
113 112 neeq1d φ p B r * x = p ball D r x p ball D r
114 df-3an g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k
115 ral0 k g k = TopOpen R k
116 difeq2 z = I I z = I I
117 difid I I =
118 116 117 eqtrdi z = I I z =
119 118 raleqdv z = I k I z g k = TopOpen R k k g k = TopOpen R k
120 119 rspcev I Fin k g k = TopOpen R k z Fin k I z g k = TopOpen R k
121 3 115 120 sylancl φ z Fin k I z g k = TopOpen R k
122 121 adantr φ p B r * z Fin k I z g k = TopOpen R k
123 122 biantrud φ p B r * g Fn I k I g k TopOpen R k g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k
124 114 123 bitr4id φ p B r * g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k g Fn I k I g k TopOpen R k
125 eqeq1 x = p ball D r x = k I g k p ball D r = k I g k
126 124 125 bi2anan9 φ p B r * x = p ball D r g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k g Fn I k I g k TopOpen R k p ball D r = k I g k
127 126 exbidv φ p B r * x = p ball D r g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k g g Fn I k I g k TopOpen R k p ball D r = k I g k
128 111 113 127 3imtr4d φ p B r * x = p ball D r x g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
129 128 ex φ p B r * x = p ball D r x g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
130 129 rexlimdvva φ p B r * x = p ball D r x g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
131 23 130 sylbid φ x ran ball D x g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
132 131 impd φ x ran ball D x g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
133 20 132 syl5bi φ x ran ball D g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
134 133 alrimiv φ x x ran ball D g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
135 ssab ran ball D x | g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k x x ran ball D g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
136 134 135 sylibr φ ran ball D x | g g Fn I k I g k TopOpen R k z Fin k I z g k = TopOpen R k x = k I g k
137 136 11 sseqtrrdi φ ran ball D C
138 ssv ∞MetSp V
139 fnssres TopOpen Fn V ∞MetSp V TopOpen ∞MetSp Fn ∞MetSp
140 12 138 139 mp2an TopOpen ∞MetSp Fn ∞MetSp
141 fvres x ∞MetSp TopOpen ∞MetSp x = TopOpen x
142 xmstps x ∞MetSp x TopSp
143 eqid TopOpen x = TopOpen x
144 143 tpstop x TopSp TopOpen x Top
145 142 144 syl x ∞MetSp TopOpen x Top
146 141 145 eqeltrd x ∞MetSp TopOpen ∞MetSp x Top
147 146 rgen x ∞MetSp TopOpen ∞MetSp x Top
148 ffnfv TopOpen ∞MetSp : ∞MetSp Top TopOpen ∞MetSp Fn ∞MetSp x ∞MetSp TopOpen ∞MetSp x Top
149 140 147 148 mpbir2an TopOpen ∞MetSp : ∞MetSp Top
150 fco2 TopOpen ∞MetSp : ∞MetSp Top R : I ∞MetSp TopOpen R : I Top
151 149 6 150 sylancr φ TopOpen R : I Top
152 eqid n I TopOpen R n = n I TopOpen R n
153 11 152 ptbasfi I Fin TopOpen R : I Top C = fi n I TopOpen R n ran m I , u TopOpen R m w n I TopOpen R n w m -1 u
154 3 151 153 syl2anc φ C = fi n I TopOpen R n ran m I , u TopOpen R m w n I TopOpen R n w m -1 u
155 eqid MetOpen D = MetOpen D
156 155 mopntop D ∞Met B MetOpen D Top
157 21 156 syl φ MetOpen D Top
158 1 5 2 3 13 prdsbas2 φ B = k I Base R k
159 6 72 sylan φ k I TopOpen R k = K
160 6 ffvelrnda φ k I R k ∞MetSp
161 xmstps R k ∞MetSp R k TopSp
162 160 161 syl φ k I R k TopSp
163 8 10 istps R k TopSp K TopOn V
164 162 163 sylib φ k I K TopOn V
165 159 164 eqeltrd φ k I TopOpen R k TopOn V
166 toponuni TopOpen R k TopOn V V = TopOpen R k
167 165 166 syl φ k I V = TopOpen R k
168 8 167 eqtr3id φ k I Base R k = TopOpen R k
169 168 ixpeq2dva φ k I Base R k = k I TopOpen R k
170 158 169 eqtrd φ B = k I TopOpen R k
171 fveq2 k = n TopOpen R k = TopOpen R n
172 171 unieqd k = n TopOpen R k = TopOpen R n
173 172 cbvixpv k I TopOpen R k = n I TopOpen R n
174 170 173 eqtrdi φ B = n I TopOpen R n
175 155 mopntopon D ∞Met B MetOpen D TopOn B
176 21 175 syl φ MetOpen D TopOn B
177 toponmax MetOpen D TopOn B B MetOpen D
178 176 177 syl φ B MetOpen D
179 174 178 eqeltrrd φ n I TopOpen R n MetOpen D
180 179 snssd φ n I TopOpen R n MetOpen D
181 174 mpteq1d φ w B w k = w n I TopOpen R n w k
182 181 ad2antrr φ k I u K w B w k = w n I TopOpen R n w k
183 182 cnveqd φ k I u K w B w k -1 = w n I TopOpen R n w k -1
184 183 imaeq1d φ k I u K w B w k -1 u = w n I TopOpen R n w k -1 u
185 fveq1 w = p w k = p k
186 185 eleq1d w = p w k u p k u
187 eqid w B w k = w B w k
188 187 mptpreima w B w k -1 u = w B | w k u
189 186 188 elrab2 p w B w k -1 u p B p k u
190 160 38 syl φ k I E ∞Met V
191 190 adantr φ k I u K p B p k u E ∞Met V
192 simprl φ k I u K p B p k u u K
193 160 74 syl φ k I K = MetOpen E
194 193 adantr φ k I u K p B p k u K = MetOpen E
195 192 194 eleqtrd φ k I u K p B p k u u MetOpen E
196 simprrr φ k I u K p B p k u p k u
197 55 mopni2 E ∞Met V u MetOpen E p k u r + p k ball E r u
198 191 195 196 197 syl3anc φ k I u K p B p k u r + p k ball E r u
199 21 ad3antrrr φ k I u K p B p k u r + p k ball E r u D ∞Met B
200 simprrl φ k I u K p B p k u p B
201 200 adantr φ k I u K p B p k u r + p k ball E r u p B
202 rpxr r + r *
203 202 ad2antrl φ k I u K p B p k u r + p k ball E r u r *
204 155 blopn D ∞Met B p B r * p ball D r MetOpen D
205 199 201 203 204 syl3anc φ k I u K p B p k u r + p k ball E r u p ball D r MetOpen D
206 simprl φ k I u K p B p k u r + p k ball E r u r +
207 blcntr D ∞Met B p B r + p p ball D r
208 199 201 206 207 syl3anc φ k I u K p B p k u r + p k ball E r u p p ball D r
209 blssm D ∞Met B p B r * p ball D r B
210 199 201 203 209 syl3anc φ k I u K p B p k u r + p k ball E r u p ball D r B
211 simplrr φ k I u K p B p k u r + p k ball E r u w p ball D r p k ball E r u
212 simplll φ k I u K p B p k u r + p k ball E r u φ
213 rpgt0 r + 0 < r
214 213 ad2antrl φ k I u K p B p k u r + p k ball E r u 0 < r
215 212 201 203 214 96 syl121anc φ k I u K p B p k u r + p k ball E r u p ball D r = k I p k ball E r
216 215 eleq2d φ k I u K p B p k u r + p k ball E r u w p ball D r w k I p k ball E r
217 216 biimpa φ k I u K p B p k u r + p k ball E r u w p ball D r w k I p k ball E r
218 vex w V
219 218 elixp w k I p k ball E r w Fn I k I w k p k ball E r
220 219 simprbi w k I p k ball E r k I w k p k ball E r
221 217 220 syl φ k I u K p B p k u r + p k ball E r u w p ball D r k I w k p k ball E r
222 simp-4r φ k I u K p B p k u r + p k ball E r u w p ball D r k I
223 rsp k I w k p k ball E r k I w k p k ball E r
224 221 222 223 sylc φ k I u K p B p k u r + p k ball E r u w p ball D r w k p k ball E r
225 211 224 sseldd φ k I u K p B p k u r + p k ball E r u w p ball D r w k u
226 210 225 ssrabdv φ k I u K p B p k u r + p k ball E r u p ball D r w B | w k u
227 226 188 sseqtrrdi φ k I u K p B p k u r + p k ball E r u p ball D r w B w k -1 u
228 eleq2 y = p ball D r p y p p ball D r
229 sseq1 y = p ball D r y w B w k -1 u p ball D r w B w k -1 u
230 228 229 anbi12d y = p ball D r p y y w B w k -1 u p p ball D r p ball D r w B w k -1 u
231 230 rspcev p ball D r MetOpen D p p ball D r p ball D r w B w k -1 u y MetOpen D p y y w B w k -1 u
232 205 208 227 231 syl12anc φ k I u K p B p k u r + p k ball E r u y MetOpen D p y y w B w k -1 u
233 198 232 rexlimddv φ k I u K p B p k u y MetOpen D p y y w B w k -1 u
234 233 expr φ k I u K p B p k u y MetOpen D p y y w B w k -1 u
235 189 234 syl5bi φ k I u K p w B w k -1 u y MetOpen D p y y w B w k -1 u
236 235 ralrimiv φ k I u K p w B w k -1 u y MetOpen D p y y w B w k -1 u
237 157 ad2antrr φ k I u K MetOpen D Top
238 eltop2 MetOpen D Top w B w k -1 u MetOpen D p w B w k -1 u y MetOpen D p y y w B w k -1 u
239 237 238 syl φ k I u K w B w k -1 u MetOpen D p w B w k -1 u y MetOpen D p y y w B w k -1 u
240 236 239 mpbird φ k I u K w B w k -1 u MetOpen D
241 184 240 eqeltrrd φ k I u K w n I TopOpen R n w k -1 u MetOpen D
242 241 ralrimiva φ k I u K w n I TopOpen R n w k -1 u MetOpen D
243 159 raleqdv φ k I u TopOpen R k w n I TopOpen R n w k -1 u MetOpen D u K w n I TopOpen R n w k -1 u MetOpen D
244 242 243 mpbird φ k I u TopOpen R k w n I TopOpen R n w k -1 u MetOpen D
245 244 ralrimiva φ k I u TopOpen R k w n I TopOpen R n w k -1 u MetOpen D
246 fveq2 k = m TopOpen R k = TopOpen R m
247 fveq2 k = m w k = w m
248 247 mpteq2dv k = m w n I TopOpen R n w k = w n I TopOpen R n w m
249 248 cnveqd k = m w n I TopOpen R n w k -1 = w n I TopOpen R n w m -1
250 249 imaeq1d k = m w n I TopOpen R n w k -1 u = w n I TopOpen R n w m -1 u
251 250 eleq1d k = m w n I TopOpen R n w k -1 u MetOpen D w n I TopOpen R n w m -1 u MetOpen D
252 246 251 raleqbidv k = m u TopOpen R k w n I TopOpen R n w k -1 u MetOpen D u TopOpen R m w n I TopOpen R n w m -1 u MetOpen D
253 252 cbvralvw k I u TopOpen R k w n I TopOpen R n w k -1 u MetOpen D m I u TopOpen R m w n I TopOpen R n w m -1 u MetOpen D
254 245 253 sylib φ m I u TopOpen R m w n I TopOpen R n w m -1 u MetOpen D
255 eqid m I , u TopOpen R m w n I TopOpen R n w m -1 u = m I , u TopOpen R m w n I TopOpen R n w m -1 u
256 255 fmpox m I u TopOpen R m w n I TopOpen R n w m -1 u MetOpen D m I , u TopOpen R m w n I TopOpen R n w m -1 u : m I m × TopOpen R m MetOpen D
257 254 256 sylib φ m I , u TopOpen R m w n I TopOpen R n w m -1 u : m I m × TopOpen R m MetOpen D
258 257 frnd φ ran m I , u TopOpen R m w n I TopOpen R n w m -1 u MetOpen D
259 180 258 unssd φ n I TopOpen R n ran m I , u TopOpen R m w n I TopOpen R n w m -1 u MetOpen D
260 fiss MetOpen D Top n I TopOpen R n ran m I , u TopOpen R m w n I TopOpen R n w m -1 u MetOpen D fi n I TopOpen R n ran m I , u TopOpen R m w n I TopOpen R n w m -1 u fi MetOpen D
261 157 259 260 syl2anc φ fi n I TopOpen R n ran m I , u TopOpen R m w n I TopOpen R n w m -1 u fi MetOpen D
262 154 261 eqsstrd φ C fi MetOpen D
263 fitop MetOpen D Top fi MetOpen D = MetOpen D
264 157 263 syl φ fi MetOpen D = MetOpen D
265 155 mopnval D ∞Met B MetOpen D = topGen ran ball D
266 21 265 syl φ MetOpen D = topGen ran ball D
267 tgdif0 topGen ran ball D = topGen ran ball D
268 266 267 eqtr4di φ MetOpen D = topGen ran ball D
269 264 268 eqtrd φ fi MetOpen D = topGen ran ball D
270 262 269 sseqtrd φ C topGen ran ball D
271 2basgen ran ball D C C topGen ran ball D topGen ran ball D = topGen C
272 137 270 271 syl2anc φ topGen ran ball D = topGen C
273 19 272 eqtr4d φ 𝑡 TopOpen R = topGen ran ball D
274 1 2 3 13 7 prdstopn φ J = 𝑡 TopOpen R
275 273 274 268 3eqtr4d φ J = MetOpen D