MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prdsxmslem2 Structured version   Visualization version   GIF version

Theorem prdsxmslem2 24258
Description: Lemma for prdsxms 24259. 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.)
Hypotheses
Ref Expression
prdsxms.y π‘Œ = (𝑆Xs𝑅)
prdsxms.s (πœ‘ β†’ 𝑆 ∈ π‘Š)
prdsxms.i (πœ‘ β†’ 𝐼 ∈ Fin)
prdsxms.d 𝐷 = (distβ€˜π‘Œ)
prdsxms.b 𝐡 = (Baseβ€˜π‘Œ)
prdsxms.r (πœ‘ β†’ 𝑅:𝐼⟢∞MetSp)
prdsxms.j 𝐽 = (TopOpenβ€˜π‘Œ)
prdsxms.v 𝑉 = (Baseβ€˜(π‘…β€˜π‘˜))
prdsxms.e 𝐸 = ((distβ€˜(π‘…β€˜π‘˜)) β†Ύ (𝑉 Γ— 𝑉))
prdsxms.k 𝐾 = (TopOpenβ€˜(π‘…β€˜π‘˜))
prdsxms.c 𝐢 = {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))}
Assertion
Ref Expression
prdsxmslem2 (πœ‘ β†’ 𝐽 = (MetOpenβ€˜π·))
Distinct variable groups:   𝑔,π‘˜,𝐡   π‘₯,𝑔,𝐷,π‘˜   𝑧,𝑔,𝐼,π‘˜,π‘₯   𝑔,𝐸   𝑆,𝑔,π‘˜,π‘₯   𝑔,π‘Š,π‘˜,π‘₯   𝑔,π‘Œ,π‘˜,π‘₯   πœ‘,𝑔,π‘˜,π‘₯   𝑅,𝑔,π‘˜,π‘₯,𝑧
Allowed substitution hints:   πœ‘(𝑧)   𝐡(π‘₯,𝑧)   𝐢(π‘₯,𝑧,𝑔,π‘˜)   𝐷(𝑧)   𝑆(𝑧)   𝐸(π‘₯,𝑧,π‘˜)   𝐽(π‘₯,𝑧,𝑔,π‘˜)   𝐾(π‘₯,𝑧,𝑔,π‘˜)   𝑉(π‘₯,𝑧,𝑔,π‘˜)   π‘Š(𝑧)   π‘Œ(𝑧)

Proof of Theorem prdsxmslem2
Dummy variables 𝑝 π‘Ÿ 𝑀 𝑦 π‘š 𝑒 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prdsxms.i . . . 4 (πœ‘ β†’ 𝐼 ∈ Fin)
2 topnfn 17375 . . . . 5 TopOpen Fn V
3 prdsxms.r . . . . . . 7 (πœ‘ β†’ 𝑅:𝐼⟢∞MetSp)
43ffnd 6717 . . . . . 6 (πœ‘ β†’ 𝑅 Fn 𝐼)
5 dffn2 6718 . . . . . 6 (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟢V)
64, 5sylib 217 . . . . 5 (πœ‘ β†’ 𝑅:𝐼⟢V)
7 fnfco 6755 . . . . 5 ((TopOpen Fn V ∧ 𝑅:𝐼⟢V) β†’ (TopOpen ∘ 𝑅) Fn 𝐼)
82, 6, 7sylancr 585 . . . 4 (πœ‘ β†’ (TopOpen ∘ 𝑅) Fn 𝐼)
9 prdsxms.c . . . . 5 𝐢 = {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))}
109ptval 23294 . . . 4 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) β†’ (∏tβ€˜(TopOpen ∘ 𝑅)) = (topGenβ€˜πΆ))
111, 8, 10syl2anc 582 . . 3 (πœ‘ β†’ (∏tβ€˜(TopOpen ∘ 𝑅)) = (topGenβ€˜πΆ))
12 eldifsn 4789 . . . . . . . 8 (π‘₯ ∈ (ran (ballβ€˜π·) βˆ– {βˆ…}) ↔ (π‘₯ ∈ ran (ballβ€˜π·) ∧ π‘₯ β‰  βˆ…))
13 prdsxms.y . . . . . . . . . . . 12 π‘Œ = (𝑆Xs𝑅)
14 prdsxms.s . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 ∈ π‘Š)
15 prdsxms.d . . . . . . . . . . . 12 𝐷 = (distβ€˜π‘Œ)
16 prdsxms.b . . . . . . . . . . . 12 𝐡 = (Baseβ€˜π‘Œ)
1713, 14, 1, 15, 16, 3prdsxmslem1 24257 . . . . . . . . . . 11 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π΅))
18 blrn 24135 . . . . . . . . . . 11 (𝐷 ∈ (∞Metβ€˜π΅) β†’ (π‘₯ ∈ ran (ballβ€˜π·) ↔ βˆƒπ‘ ∈ 𝐡 βˆƒπ‘Ÿ ∈ ℝ* π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)))
1917, 18syl 17 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ ran (ballβ€˜π·) ↔ βˆƒπ‘ ∈ 𝐡 βˆƒπ‘Ÿ ∈ ℝ* π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)))
2017adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ 𝐷 ∈ (∞Metβ€˜π΅))
21 simprl 767 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ 𝑝 ∈ 𝐡)
22 simprr 769 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ π‘Ÿ ∈ ℝ*)
23 xbln0 24140 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Metβ€˜π΅) ∧ 𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ… ↔ 0 < π‘Ÿ))
2420, 21, 22, 23syl3anc 1369 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ… ↔ 0 < π‘Ÿ))
2513ad2ant1 1131 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝐼 ∈ Fin)
2625mptexd 7227 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) ∈ V)
27 ovex 7444 . . . . . . . . . . . . . . . . . . 19 ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ) ∈ V
2827rgenw 3063 . . . . . . . . . . . . . . . . . 18 βˆ€π‘› ∈ 𝐼 ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ) ∈ V
29 eqid 2730 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))
3029fnmpt 6689 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ 𝐼 ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ) ∈ V β†’ (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼)
3128, 30mp1i 13 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼)
3233ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑅:𝐼⟢∞MetSp)
3332ffvelcdmda 7085 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ (π‘…β€˜π‘˜) ∈ ∞MetSp)
34 prdsxms.v . . . . . . . . . . . . . . . . . . . . . 22 𝑉 = (Baseβ€˜(π‘…β€˜π‘˜))
35 prdsxms.e . . . . . . . . . . . . . . . . . . . . . 22 𝐸 = ((distβ€˜(π‘…β€˜π‘˜)) β†Ύ (𝑉 Γ— 𝑉))
3634, 35xmsxmet 24182 . . . . . . . . . . . . . . . . . . . . 21 ((π‘…β€˜π‘˜) ∈ ∞MetSp β†’ 𝐸 ∈ (∞Metβ€˜π‘‰))
3733, 36syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ 𝐸 ∈ (∞Metβ€˜π‘‰))
38 eqid 2730 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))) = (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))
39 eqid 2730 . . . . . . . . . . . . . . . . . . . . . 22 (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))) = (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))))
40143ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑆 ∈ π‘Š)
4133ralrimiva 3144 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ βˆ€π‘˜ ∈ 𝐼 (π‘…β€˜π‘˜) ∈ ∞MetSp)
42 simp2l 1197 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑝 ∈ 𝐡)
4332feqmptd 6959 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑅 = (π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))
4443oveq2d 7427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑆Xs𝑅) = (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))))
4513, 44eqtrid 2782 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ π‘Œ = (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))))
4645fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (Baseβ€˜π‘Œ) = (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))))
4716, 46eqtrid 2782 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝐡 = (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))))
4842, 47eleqtrd 2833 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑝 ∈ (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))))
4938, 39, 40, 25, 41, 34, 48prdsbascl 17433 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ βˆ€π‘˜ ∈ 𝐼 (π‘β€˜π‘˜) ∈ 𝑉)
5049r19.21bi 3246 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ (π‘β€˜π‘˜) ∈ 𝑉)
51 simp2r 1198 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ π‘Ÿ ∈ ℝ*)
5251adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ π‘Ÿ ∈ ℝ*)
53 eqid 2730 . . . . . . . . . . . . . . . . . . . . 21 (MetOpenβ€˜πΈ) = (MetOpenβ€˜πΈ)
5453blopn 24229 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Metβ€˜π‘‰) ∧ (π‘β€˜π‘˜) ∈ 𝑉 ∧ π‘Ÿ ∈ ℝ*) β†’ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) ∈ (MetOpenβ€˜πΈ))
5537, 50, 52, 54syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) ∈ (MetOpenβ€˜πΈ))
56 2fveq3 6895 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = π‘˜ β†’ (distβ€˜(π‘…β€˜π‘›)) = (distβ€˜(π‘…β€˜π‘˜)))
57 2fveq3 6895 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = π‘˜ β†’ (Baseβ€˜(π‘…β€˜π‘›)) = (Baseβ€˜(π‘…β€˜π‘˜)))
5857, 34eqtr4di 2788 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = π‘˜ β†’ (Baseβ€˜(π‘…β€˜π‘›)) = 𝑉)
5958sqxpeqd 5707 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = π‘˜ β†’ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›))) = (𝑉 Γ— 𝑉))
6056, 59reseq12d 5981 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = π‘˜ β†’ ((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))) = ((distβ€˜(π‘…β€˜π‘˜)) β†Ύ (𝑉 Γ— 𝑉)))
6160, 35eqtr4di 2788 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = π‘˜ β†’ ((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))) = 𝐸)
6261fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = π‘˜ β†’ (ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›))))) = (ballβ€˜πΈ))
63 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = π‘˜ β†’ (π‘β€˜π‘›) = (π‘β€˜π‘˜))
64 eqidd 2731 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = π‘˜ β†’ π‘Ÿ = π‘Ÿ)
6562, 63, 64oveq123d 7432 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = π‘˜ β†’ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ) = ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
66 ovex 7444 . . . . . . . . . . . . . . . . . . . . 21 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) ∈ V
6765, 29, 66fvmpt 6997 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ 𝐼 β†’ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) = ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
6867adantl 480 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) = ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
69 fvco3 6989 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅:𝐼⟢∞MetSp ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = (TopOpenβ€˜(π‘…β€˜π‘˜)))
70 prdsxms.k . . . . . . . . . . . . . . . . . . . . . 22 𝐾 = (TopOpenβ€˜(π‘…β€˜π‘˜))
7169, 70eqtr4di 2788 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅:𝐼⟢∞MetSp ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = 𝐾)
7232, 71sylan 578 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = 𝐾)
7370, 34, 35xmstopn 24177 . . . . . . . . . . . . . . . . . . . . 21 ((π‘…β€˜π‘˜) ∈ ∞MetSp β†’ 𝐾 = (MetOpenβ€˜πΈ))
7433, 73syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ 𝐾 = (MetOpenβ€˜πΈ))
7572, 74eqtrd 2770 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = (MetOpenβ€˜πΈ))
7655, 68, 753eltr4d 2846 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜))
7776ralrimiva 3144 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜))
7832feqmptd 6959 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑅 = (𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))
7978oveq2d 7427 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑆Xs𝑅) = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))
8013, 79eqtrid 2782 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ π‘Œ = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))
8180fveq2d 6894 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (distβ€˜π‘Œ) = (distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
8215, 81eqtrid 2782 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝐷 = (distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
8382fveq2d 6894 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (ballβ€˜π·) = (ballβ€˜(distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))))
8483oveqd 7428 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) = (𝑝(ballβ€˜(distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))π‘Ÿ))
85 fveq2 6890 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = π‘˜ β†’ (π‘…β€˜π‘›) = (π‘…β€˜π‘˜))
8685cbvmptv 5260 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)) = (π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))
8786oveq2i 7422 . . . . . . . . . . . . . . . . . . 19 (𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))) = (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))
88 eqid 2730 . . . . . . . . . . . . . . . . . . 19 (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))) = (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))
89 eqid 2730 . . . . . . . . . . . . . . . . . . 19 (distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))) = (distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))
9080fveq2d 6894 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (Baseβ€˜π‘Œ) = (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
9116, 90eqtrid 2782 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝐡 = (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
9242, 91eleqtrd 2833 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑝 ∈ (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
93 simp3 1136 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 0 < π‘Ÿ)
9487, 88, 34, 35, 89, 40, 25, 33, 37, 92, 51, 93prdsbl 24220 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑝(ballβ€˜(distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
9584, 94eqtrd 2770 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
96 fneq1 6639 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ (𝑔 Fn 𝐼 ↔ (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼))
97 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ (π‘”β€˜π‘˜) = ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜))
9897eleq1d 2816 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ ((π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ↔ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)))
9998ralbidv 3175 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ (βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)))
10096, 99anbi12d 629 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ↔ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜))))
10197, 67sylan9eq 2790 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) ∧ π‘˜ ∈ 𝐼) β†’ (π‘”β€˜π‘˜) = ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
102101ixpeq2dva 8908 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
103102eqeq2d 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ↔ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)))
104100, 103anbi12d 629 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)) ↔ (((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))))
105104spcegv 3586 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) ∈ V β†’ ((((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
1061053impib 1114 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) ∈ V ∧ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
10726, 31, 77, 95, 106syl121anc 1373 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
1081073expia 1119 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ (0 < π‘Ÿ β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
10924, 108sylbid 239 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
110109adantr 479 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
111 simpr 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ))
112111neeq1d 2998 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (π‘₯ β‰  βˆ… ↔ (𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ…))
113 df-3an 1087 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)))
114 ral0 4511 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘˜ ∈ βˆ… (π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)
115 difeq2 4115 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝐼 β†’ (𝐼 βˆ– 𝑧) = (𝐼 βˆ– 𝐼))
116 difid 4369 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼 βˆ– 𝐼) = βˆ…
117115, 116eqtrdi 2786 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝐼 β†’ (𝐼 βˆ– 𝑧) = βˆ…)
118117raleqdv 3323 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝐼 β†’ (βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜) ↔ βˆ€π‘˜ ∈ βˆ… (π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)))
119118rspcev 3611 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ Fin ∧ βˆ€π‘˜ ∈ βˆ… (π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) β†’ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
1201, 114, 119sylancl 584 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
121120adantr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
122121biantrud 530 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))))
123113, 122bitr4id 289 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ↔ (𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜))))
124 eqeq1 2734 . . . . . . . . . . . . . . 15 (π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ↔ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
125123, 124bi2anan9 635 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
126125exbidv 1922 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)) ↔ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
127110, 112, 1263imtr4d 293 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (π‘₯ β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
128127ex 411 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ (π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (π‘₯ β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
129128rexlimdvva 3209 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘ ∈ 𝐡 βˆƒπ‘Ÿ ∈ ℝ* π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (π‘₯ β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
13019, 129sylbid 239 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ ran (ballβ€˜π·) β†’ (π‘₯ β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
131130impd 409 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ ran (ballβ€˜π·) ∧ π‘₯ β‰  βˆ…) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
13212, 131biimtrid 241 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (ran (ballβ€˜π·) βˆ– {βˆ…}) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
133132alrimiv 1928 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯(π‘₯ ∈ (ran (ballβ€˜π·) βˆ– {βˆ…}) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
134 ssab 4057 . . . . . 6 ((ran (ballβ€˜π·) βˆ– {βˆ…}) βŠ† {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))} ↔ βˆ€π‘₯(π‘₯ ∈ (ran (ballβ€˜π·) βˆ– {βˆ…}) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
135133, 134sylibr 233 . . . . 5 (πœ‘ β†’ (ran (ballβ€˜π·) βˆ– {βˆ…}) βŠ† {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))})
136135, 9sseqtrrdi 4032 . . . 4 (πœ‘ β†’ (ran (ballβ€˜π·) βˆ– {βˆ…}) βŠ† 𝐢)
137 ssv 4005 . . . . . . . . . 10 ∞MetSp βŠ† V
138 fnssres 6672 . . . . . . . . . 10 ((TopOpen Fn V ∧ ∞MetSp βŠ† V) β†’ (TopOpen β†Ύ ∞MetSp) Fn ∞MetSp)
1392, 137, 138mp2an 688 . . . . . . . . 9 (TopOpen β†Ύ ∞MetSp) Fn ∞MetSp
140 fvres 6909 . . . . . . . . . . 11 (π‘₯ ∈ ∞MetSp β†’ ((TopOpen β†Ύ ∞MetSp)β€˜π‘₯) = (TopOpenβ€˜π‘₯))
141 xmstps 24179 . . . . . . . . . . . 12 (π‘₯ ∈ ∞MetSp β†’ π‘₯ ∈ TopSp)
142 eqid 2730 . . . . . . . . . . . . 13 (TopOpenβ€˜π‘₯) = (TopOpenβ€˜π‘₯)
143142tpstop 22659 . . . . . . . . . . . 12 (π‘₯ ∈ TopSp β†’ (TopOpenβ€˜π‘₯) ∈ Top)
144141, 143syl 17 . . . . . . . . . . 11 (π‘₯ ∈ ∞MetSp β†’ (TopOpenβ€˜π‘₯) ∈ Top)
145140, 144eqeltrd 2831 . . . . . . . . . 10 (π‘₯ ∈ ∞MetSp β†’ ((TopOpen β†Ύ ∞MetSp)β€˜π‘₯) ∈ Top)
146145rgen 3061 . . . . . . . . 9 βˆ€π‘₯ ∈ ∞MetSp ((TopOpen β†Ύ ∞MetSp)β€˜π‘₯) ∈ Top
147 ffnfv 7119 . . . . . . . . 9 ((TopOpen β†Ύ ∞MetSp):∞MetSp⟢Top ↔ ((TopOpen β†Ύ ∞MetSp) Fn ∞MetSp ∧ βˆ€π‘₯ ∈ ∞MetSp ((TopOpen β†Ύ ∞MetSp)β€˜π‘₯) ∈ Top))
148139, 146, 147mpbir2an 707 . . . . . . . 8 (TopOpen β†Ύ ∞MetSp):∞MetSp⟢Top
149 fco2 6743 . . . . . . . 8 (((TopOpen β†Ύ ∞MetSp):∞MetSp⟢Top ∧ 𝑅:𝐼⟢∞MetSp) β†’ (TopOpen ∘ 𝑅):𝐼⟢Top)
150148, 3, 149sylancr 585 . . . . . . 7 (πœ‘ β†’ (TopOpen ∘ 𝑅):𝐼⟢Top)
151 eqid 2730 . . . . . . . 8 X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) = X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)
1529, 151ptbasfi 23305 . . . . . . 7 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅):𝐼⟢Top) β†’ 𝐢 = (fiβ€˜({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)))))
1531, 150, 152syl2anc 582 . . . . . 6 (πœ‘ β†’ 𝐢 = (fiβ€˜({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)))))
154 eqid 2730 . . . . . . . . 9 (MetOpenβ€˜π·) = (MetOpenβ€˜π·)
155154mopntop 24166 . . . . . . . 8 (𝐷 ∈ (∞Metβ€˜π΅) β†’ (MetOpenβ€˜π·) ∈ Top)
15617, 155syl 17 . . . . . . 7 (πœ‘ β†’ (MetOpenβ€˜π·) ∈ Top)
15713, 16, 14, 1, 4prdsbas2 17419 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 = Xπ‘˜ ∈ 𝐼 (Baseβ€˜(π‘…β€˜π‘˜)))
1583, 71sylan 578 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = 𝐾)
1593ffvelcdmda 7085 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘…β€˜π‘˜) ∈ ∞MetSp)
160 xmstps 24179 . . . . . . . . . . . . . . . . . 18 ((π‘…β€˜π‘˜) ∈ ∞MetSp β†’ (π‘…β€˜π‘˜) ∈ TopSp)
161159, 160syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘…β€˜π‘˜) ∈ TopSp)
16234, 70istps 22656 . . . . . . . . . . . . . . . . 17 ((π‘…β€˜π‘˜) ∈ TopSp ↔ 𝐾 ∈ (TopOnβ€˜π‘‰))
163161, 162sylib 217 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐾 ∈ (TopOnβ€˜π‘‰))
164158, 163eqeltrd 2831 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∈ (TopOnβ€˜π‘‰))
165 toponuni 22636 . . . . . . . . . . . . . . 15 (((TopOpen ∘ 𝑅)β€˜π‘˜) ∈ (TopOnβ€˜π‘‰) β†’ 𝑉 = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
166164, 165syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝑉 = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
16734, 166eqtr3id 2784 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (Baseβ€˜(π‘…β€˜π‘˜)) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
168167ixpeq2dva 8908 . . . . . . . . . . . 12 (πœ‘ β†’ Xπ‘˜ ∈ 𝐼 (Baseβ€˜(π‘…β€˜π‘˜)) = Xπ‘˜ ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
169157, 168eqtrd 2770 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 = Xπ‘˜ ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
170 fveq2 6890 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = ((TopOpen ∘ 𝑅)β€˜π‘›))
171170unieqd 4921 . . . . . . . . . . . 12 (π‘˜ = 𝑛 β†’ βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›))
172171cbvixpv 8911 . . . . . . . . . . 11 Xπ‘˜ ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜) = X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)
173169, 172eqtrdi 2786 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 = X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›))
174154mopntopon 24165 . . . . . . . . . . . 12 (𝐷 ∈ (∞Metβ€˜π΅) β†’ (MetOpenβ€˜π·) ∈ (TopOnβ€˜π΅))
17517, 174syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (MetOpenβ€˜π·) ∈ (TopOnβ€˜π΅))
176 toponmax 22648 . . . . . . . . . . 11 ((MetOpenβ€˜π·) ∈ (TopOnβ€˜π΅) β†’ 𝐡 ∈ (MetOpenβ€˜π·))
177175, 176syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ (MetOpenβ€˜π·))
178173, 177eqeltrrd 2832 . . . . . . . . 9 (πœ‘ β†’ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ∈ (MetOpenβ€˜π·))
179178snssd 4811 . . . . . . . 8 (πœ‘ β†’ {X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βŠ† (MetOpenβ€˜π·))
180173mpteq1d 5242 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)))
181180ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)))
182181cnveqd 5874 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) = β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)))
183182imaeq1d 6057 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
184 fveq1 6889 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = 𝑝 β†’ (π‘€β€˜π‘˜) = (π‘β€˜π‘˜))
185184eleq1d 2816 . . . . . . . . . . . . . . . . . . 19 (𝑀 = 𝑝 β†’ ((π‘€β€˜π‘˜) ∈ 𝑒 ↔ (π‘β€˜π‘˜) ∈ 𝑒))
186 eqid 2730 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜))
187186mptpreima 6236 . . . . . . . . . . . . . . . . . . 19 (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = {𝑀 ∈ 𝐡 ∣ (π‘€β€˜π‘˜) ∈ 𝑒}
188185, 187elrab2 3685 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))
189159, 36syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐸 ∈ (∞Metβ€˜π‘‰))
190189adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝐸 ∈ (∞Metβ€˜π‘‰))
191 simprl 767 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝑒 ∈ 𝐾)
192159, 73syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐾 = (MetOpenβ€˜πΈ))
193192adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝐾 = (MetOpenβ€˜πΈ))
194191, 193eleqtrd 2833 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝑒 ∈ (MetOpenβ€˜πΈ))
195 simprrr 778 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ (π‘β€˜π‘˜) ∈ 𝑒)
19653mopni2 24222 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Metβ€˜π‘‰) ∧ 𝑒 ∈ (MetOpenβ€˜πΈ) ∧ (π‘β€˜π‘˜) ∈ 𝑒) β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)
197190, 194, 195, 196syl3anc 1369 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)
19817ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ 𝐷 ∈ (∞Metβ€˜π΅))
199 simprrl 777 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝑝 ∈ 𝐡)
200199adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ 𝑝 ∈ 𝐡)
201 rpxr 12987 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ*)
202201ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ π‘Ÿ ∈ ℝ*)
203154blopn 24229 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Metβ€˜π΅) ∧ 𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) ∈ (MetOpenβ€˜π·))
204198, 200, 202, 203syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) ∈ (MetOpenβ€˜π·))
205 simprl 767 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ π‘Ÿ ∈ ℝ+)
206 blcntr 24139 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Metβ€˜π΅) ∧ 𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ))
207198, 200, 205, 206syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ 𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ))
208 blssm 24144 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (∞Metβ€˜π΅) ∧ 𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† 𝐡)
209198, 200, 202, 208syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† 𝐡)
210 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)
211 simplll 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ πœ‘)
212 rpgt0 12990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘Ÿ ∈ ℝ+ β†’ 0 < π‘Ÿ)
213212ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ 0 < π‘Ÿ)
214211, 200, 202, 213, 95syl121anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
215214eleq2d 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ) ↔ 𝑀 ∈ Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)))
216215biimpa 475 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ 𝑀 ∈ Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
217 vex 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑀 ∈ V
218217elixp 8900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) ↔ (𝑀 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)))
219218simprbi 495 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 ∈ Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) β†’ βˆ€π‘˜ ∈ 𝐼 (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
220216, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ βˆ€π‘˜ ∈ 𝐼 (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
221 simp-4r 780 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ π‘˜ ∈ 𝐼)
222 rsp 3242 . . . . . . . . . . . . . . . . . . . . . . . . 25 (βˆ€π‘˜ ∈ 𝐼 (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) β†’ (π‘˜ ∈ 𝐼 β†’ (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)))
223220, 221, 222sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
224210, 223sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (π‘€β€˜π‘˜) ∈ 𝑒)
225209, 224ssrabdv 4070 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† {𝑀 ∈ 𝐡 ∣ (π‘€β€˜π‘˜) ∈ 𝑒})
226225, 187sseqtrrdi 4032 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
227 eleq2 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (𝑝 ∈ 𝑦 ↔ 𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)))
228 sseq1 4006 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
229227, 228anbi12d 629 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ ((𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ↔ (𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
230229rspcev 3611 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝(ballβ€˜π·)π‘Ÿ) ∈ (MetOpenβ€˜π·) ∧ (𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
231204, 207, 226, 230syl12anc 833 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
232197, 231rexlimddv 3159 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
233232expr 455 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ ((𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
234188, 233biimtrid 241 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (𝑝 ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
235234ralrimiv 3143 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ βˆ€π‘ ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
236156ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (MetOpenβ€˜π·) ∈ Top)
237 eltop2 22698 . . . . . . . . . . . . . . . . 17 ((MetOpenβ€˜π·) ∈ Top β†’ ((β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘ ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
238236, 237syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ ((β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘ ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
239235, 238mpbird 256 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
240183, 239eqeltrrd 2832 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
241240ralrimiva 3144 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘’ ∈ 𝐾 (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
242158raleqdv 3323 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘’ ∈ 𝐾 (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·)))
243241, 242mpbird 256 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
244243ralrimiva 3144 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
245 fveq2 6890 . . . . . . . . . . . . 13 (π‘˜ = π‘š β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = ((TopOpen ∘ 𝑅)β€˜π‘š))
246 fveq2 6890 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘š β†’ (π‘€β€˜π‘˜) = (π‘€β€˜π‘š))
247246mpteq2dv 5249 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘š β†’ (𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)))
248247cnveqd 5874 . . . . . . . . . . . . . . 15 (π‘˜ = π‘š β†’ β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)))
249248imaeq1d 6057 . . . . . . . . . . . . . 14 (π‘˜ = π‘š β†’ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒))
250249eleq1d 2816 . . . . . . . . . . . . 13 (π‘˜ = π‘š β†’ ((β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·)))
251245, 250raleqbidv 3340 . . . . . . . . . . . 12 (π‘˜ = π‘š β†’ (βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘š)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·)))
252251cbvralvw 3232 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘š ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘š)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
253244, 252sylib 217 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘š ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘š)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
254 eqid 2730 . . . . . . . . . . 11 (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)) = (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒))
255254fmpox 8055 . . . . . . . . . 10 (βˆ€π‘š ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘š)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)):βˆͺ π‘š ∈ 𝐼 ({π‘š} Γ— ((TopOpen ∘ 𝑅)β€˜π‘š))⟢(MetOpenβ€˜π·))
256253, 255sylib 217 . . . . . . . . 9 (πœ‘ β†’ (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)):βˆͺ π‘š ∈ 𝐼 ({π‘š} Γ— ((TopOpen ∘ 𝑅)β€˜π‘š))⟢(MetOpenβ€˜π·))
257256frnd 6724 . . . . . . . 8 (πœ‘ β†’ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)) βŠ† (MetOpenβ€˜π·))
258179, 257unssd 4185 . . . . . . 7 (πœ‘ β†’ ({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒))) βŠ† (MetOpenβ€˜π·))
259 fiss 9421 . . . . . . 7 (((MetOpenβ€˜π·) ∈ Top ∧ ({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒))) βŠ† (MetOpenβ€˜π·)) β†’ (fiβ€˜({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)))) βŠ† (fiβ€˜(MetOpenβ€˜π·)))
260156, 258, 259syl2anc 582 . . . . . 6 (πœ‘ β†’ (fiβ€˜({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)))) βŠ† (fiβ€˜(MetOpenβ€˜π·)))
261153, 260eqsstrd 4019 . . . . 5 (πœ‘ β†’ 𝐢 βŠ† (fiβ€˜(MetOpenβ€˜π·)))
262 fitop 22622 . . . . . . 7 ((MetOpenβ€˜π·) ∈ Top β†’ (fiβ€˜(MetOpenβ€˜π·)) = (MetOpenβ€˜π·))
263156, 262syl 17 . . . . . 6 (πœ‘ β†’ (fiβ€˜(MetOpenβ€˜π·)) = (MetOpenβ€˜π·))
264154mopnval 24164 . . . . . . . 8 (𝐷 ∈ (∞Metβ€˜π΅) β†’ (MetOpenβ€˜π·) = (topGenβ€˜ran (ballβ€˜π·)))
26517, 264syl 17 . . . . . . 7 (πœ‘ β†’ (MetOpenβ€˜π·) = (topGenβ€˜ran (ballβ€˜π·)))
266 tgdif0 22715 . . . . . . 7 (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})) = (topGenβ€˜ran (ballβ€˜π·))
267265, 266eqtr4di 2788 . . . . . 6 (πœ‘ β†’ (MetOpenβ€˜π·) = (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})))
268263, 267eqtrd 2770 . . . . 5 (πœ‘ β†’ (fiβ€˜(MetOpenβ€˜π·)) = (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})))
269261, 268sseqtrd 4021 . . . 4 (πœ‘ β†’ 𝐢 βŠ† (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})))
270 2basgen 22713 . . . 4 (((ran (ballβ€˜π·) βˆ– {βˆ…}) βŠ† 𝐢 ∧ 𝐢 βŠ† (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…}))) β†’ (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})) = (topGenβ€˜πΆ))
271136, 269, 270syl2anc 582 . . 3 (πœ‘ β†’ (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})) = (topGenβ€˜πΆ))
27211, 271eqtr4d 2773 . 2 (πœ‘ β†’ (∏tβ€˜(TopOpen ∘ 𝑅)) = (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})))
273 prdsxms.j . . 3 𝐽 = (TopOpenβ€˜π‘Œ)
27413, 14, 1, 4, 273prdstopn 23352 . 2 (πœ‘ β†’ 𝐽 = (∏tβ€˜(TopOpen ∘ 𝑅)))
275272, 274, 2673eqtr4d 2780 1 (πœ‘ β†’ 𝐽 = (MetOpenβ€˜π·))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085  βˆ€wal 1537   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104  {cab 2707   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  βˆͺ cuni 4907  βˆͺ ciun 4996   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673  β—‘ccnv 5674  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   ∘ ccom 5679   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ∈ cmpo 7413  Xcixp 8893  Fincfn 8941  ficfi 9407  0cc0 11112  β„*cxr 11251   < clt 11252  β„+crp 12978  Basecbs 17148  distcds 17210  TopOpenctopn 17371  topGenctg 17387  βˆtcpt 17388  Xscprds 17395  βˆžMetcxmet 21129  ballcbl 21131  MetOpencmopn 21134  Topctop 22615  TopOnctopon 22632  TopSpctps 22654  βˆžMetSpcxms 24043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9408  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-icc 13335  df-fz 13489  df-struct 17084  df-slot 17119  df-ndx 17131  df-base 17149  df-plusg 17214  df-mulr 17215  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-hom 17225  df-cco 17226  df-rest 17372  df-topn 17373  df-topgen 17393  df-pt 17394  df-prds 17397  df-psmet 21136  df-xmet 21137  df-bl 21139  df-mopn 21140  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-xms 24046
This theorem is referenced by:  prdsxms  24259
  Copyright terms: Public domain W3C validator