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

Theorem prdsxmslem2 24038
Description: Lemma for prdsxms 24039. 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 17371 . . . . 5 TopOpen Fn V
3 prdsxms.r . . . . . . 7 (πœ‘ β†’ 𝑅:𝐼⟢∞MetSp)
43ffnd 6719 . . . . . 6 (πœ‘ β†’ 𝑅 Fn 𝐼)
5 dffn2 6720 . . . . . 6 (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟢V)
64, 5sylib 217 . . . . 5 (πœ‘ β†’ 𝑅:𝐼⟢V)
7 fnfco 6757 . . . . 5 ((TopOpen Fn V ∧ 𝑅:𝐼⟢V) β†’ (TopOpen ∘ 𝑅) Fn 𝐼)
82, 6, 7sylancr 588 . . . 4 (πœ‘ β†’ (TopOpen ∘ 𝑅) Fn 𝐼)
9 prdsxms.c . . . . 5 𝐢 = {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))}
109ptval 23074 . . . 4 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) β†’ (∏tβ€˜(TopOpen ∘ 𝑅)) = (topGenβ€˜πΆ))
111, 8, 10syl2anc 585 . . 3 (πœ‘ β†’ (∏tβ€˜(TopOpen ∘ 𝑅)) = (topGenβ€˜πΆ))
12 eldifsn 4791 . . . . . . . 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 24037 . . . . . . . . . . 11 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π΅))
18 blrn 23915 . . . . . . . . . . 11 (𝐷 ∈ (∞Metβ€˜π΅) β†’ (π‘₯ ∈ ran (ballβ€˜π·) ↔ βˆƒπ‘ ∈ 𝐡 βˆƒπ‘Ÿ ∈ ℝ* π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)))
1917, 18syl 17 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ ran (ballβ€˜π·) ↔ βˆƒπ‘ ∈ 𝐡 βˆƒπ‘Ÿ ∈ ℝ* π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)))
2017adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ 𝐷 ∈ (∞Metβ€˜π΅))
21 simprl 770 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ 𝑝 ∈ 𝐡)
22 simprr 772 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ π‘Ÿ ∈ ℝ*)
23 xbln0 23920 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Metβ€˜π΅) ∧ 𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ… ↔ 0 < π‘Ÿ))
2420, 21, 22, 23syl3anc 1372 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ… ↔ 0 < π‘Ÿ))
2513ad2ant1 1134 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝐼 ∈ Fin)
2625mptexd 7226 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) ∈ V)
27 ovex 7442 . . . . . . . . . . . . . . . . . . 19 ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ) ∈ V
2827rgenw 3066 . . . . . . . . . . . . . . . . . 18 βˆ€π‘› ∈ 𝐼 ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ) ∈ V
29 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))
3029fnmpt 6691 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ 𝐼 ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ) ∈ V β†’ (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼)
3128, 30mp1i 13 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼)
3233ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑅:𝐼⟢∞MetSp)
3332ffvelcdmda 7087 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ (π‘…β€˜π‘˜) ∈ ∞MetSp)
34 prdsxms.v . . . . . . . . . . . . . . . . . . . . . 22 𝑉 = (Baseβ€˜(π‘…β€˜π‘˜))
35 prdsxms.e . . . . . . . . . . . . . . . . . . . . . 22 𝐸 = ((distβ€˜(π‘…β€˜π‘˜)) β†Ύ (𝑉 Γ— 𝑉))
3634, 35xmsxmet 23962 . . . . . . . . . . . . . . . . . . . . 21 ((π‘…β€˜π‘˜) ∈ ∞MetSp β†’ 𝐸 ∈ (∞Metβ€˜π‘‰))
3733, 36syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ 𝐸 ∈ (∞Metβ€˜π‘‰))
38 eqid 2733 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))) = (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))
39 eqid 2733 . . . . . . . . . . . . . . . . . . . . . 22 (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))) = (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))))
40143ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑆 ∈ π‘Š)
4133ralrimiva 3147 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ βˆ€π‘˜ ∈ 𝐼 (π‘…β€˜π‘˜) ∈ ∞MetSp)
42 simp2l 1200 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑝 ∈ 𝐡)
4332feqmptd 6961 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑅 = (π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))
4443oveq2d 7425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑆Xs𝑅) = (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))))
4513, 44eqtrid 2785 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ π‘Œ = (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))))
4645fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (Baseβ€˜π‘Œ) = (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))))
4716, 46eqtrid 2785 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝐡 = (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))))
4842, 47eleqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑝 ∈ (Baseβ€˜(𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))))
4938, 39, 40, 25, 41, 34, 48prdsbascl 17429 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ βˆ€π‘˜ ∈ 𝐼 (π‘β€˜π‘˜) ∈ 𝑉)
5049r19.21bi 3249 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ (π‘β€˜π‘˜) ∈ 𝑉)
51 simp2r 1201 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ π‘Ÿ ∈ ℝ*)
5251adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ π‘Ÿ ∈ ℝ*)
53 eqid 2733 . . . . . . . . . . . . . . . . . . . . 21 (MetOpenβ€˜πΈ) = (MetOpenβ€˜πΈ)
5453blopn 24009 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Metβ€˜π‘‰) ∧ (π‘β€˜π‘˜) ∈ 𝑉 ∧ π‘Ÿ ∈ ℝ*) β†’ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) ∈ (MetOpenβ€˜πΈ))
5537, 50, 52, 54syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) ∈ (MetOpenβ€˜πΈ))
56 2fveq3 6897 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = π‘˜ β†’ (distβ€˜(π‘…β€˜π‘›)) = (distβ€˜(π‘…β€˜π‘˜)))
57 2fveq3 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = π‘˜ β†’ (Baseβ€˜(π‘…β€˜π‘›)) = (Baseβ€˜(π‘…β€˜π‘˜)))
5857, 34eqtr4di 2791 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = π‘˜ β†’ (Baseβ€˜(π‘…β€˜π‘›)) = 𝑉)
5958sqxpeqd 5709 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = π‘˜ β†’ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›))) = (𝑉 Γ— 𝑉))
6056, 59reseq12d 5983 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = π‘˜ β†’ ((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))) = ((distβ€˜(π‘…β€˜π‘˜)) β†Ύ (𝑉 Γ— 𝑉)))
6160, 35eqtr4di 2791 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = π‘˜ β†’ ((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))) = 𝐸)
6261fveq2d 6896 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = π‘˜ β†’ (ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›))))) = (ballβ€˜πΈ))
63 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = π‘˜ β†’ (π‘β€˜π‘›) = (π‘β€˜π‘˜))
64 eqidd 2734 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = π‘˜ β†’ π‘Ÿ = π‘Ÿ)
6562, 63, 64oveq123d 7430 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = π‘˜ β†’ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ) = ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
66 ovex 7442 . . . . . . . . . . . . . . . . . . . . 21 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) ∈ V
6765, 29, 66fvmpt 6999 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ 𝐼 β†’ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) = ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
6867adantl 483 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) = ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
69 fvco3 6991 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅:𝐼⟢∞MetSp ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = (TopOpenβ€˜(π‘…β€˜π‘˜)))
70 prdsxms.k . . . . . . . . . . . . . . . . . . . . . 22 𝐾 = (TopOpenβ€˜(π‘…β€˜π‘˜))
7169, 70eqtr4di 2791 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅:𝐼⟢∞MetSp ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = 𝐾)
7232, 71sylan 581 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = 𝐾)
7370, 34, 35xmstopn 23957 . . . . . . . . . . . . . . . . . . . . 21 ((π‘…β€˜π‘˜) ∈ ∞MetSp β†’ 𝐾 = (MetOpenβ€˜πΈ))
7433, 73syl 17 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ 𝐾 = (MetOpenβ€˜πΈ))
7572, 74eqtrd 2773 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = (MetOpenβ€˜πΈ))
7655, 68, 753eltr4d 2849 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) ∧ π‘˜ ∈ 𝐼) β†’ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜))
7776ralrimiva 3147 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜))
7832feqmptd 6961 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑅 = (𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))
7978oveq2d 7425 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑆Xs𝑅) = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))
8013, 79eqtrid 2785 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ π‘Œ = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))
8180fveq2d 6896 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (distβ€˜π‘Œ) = (distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
8215, 81eqtrid 2785 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝐷 = (distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
8382fveq2d 6896 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (ballβ€˜π·) = (ballβ€˜(distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))))
8483oveqd 7426 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) = (𝑝(ballβ€˜(distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))π‘Ÿ))
85 fveq2 6892 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = π‘˜ β†’ (π‘…β€˜π‘›) = (π‘…β€˜π‘˜))
8685cbvmptv 5262 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)) = (π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜))
8786oveq2i 7420 . . . . . . . . . . . . . . . . . . 19 (𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))) = (𝑆Xs(π‘˜ ∈ 𝐼 ↦ (π‘…β€˜π‘˜)))
88 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))) = (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))
89 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))) = (distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›))))
9080fveq2d 6896 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (Baseβ€˜π‘Œ) = (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
9116, 90eqtrid 2785 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝐡 = (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
9242, 91eleqtrd 2836 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 𝑝 ∈ (Baseβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))
93 simp3 1139 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ 0 < π‘Ÿ)
9487, 88, 34, 35, 89, 40, 25, 33, 37, 92, 51, 93prdsbl 24000 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑝(ballβ€˜(distβ€˜(𝑆Xs(𝑛 ∈ 𝐼 ↦ (π‘…β€˜π‘›)))))π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
9584, 94eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
96 fneq1 6641 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ (𝑔 Fn 𝐼 ↔ (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼))
97 fveq1 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ (π‘”β€˜π‘˜) = ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜))
9897eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ ((π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ↔ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)))
9998ralbidv 3178 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ (βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)))
10096, 99anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ↔ ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜))))
10197, 67sylan9eq 2793 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) ∧ π‘˜ ∈ 𝐼) β†’ (π‘”β€˜π‘˜) = ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
102101ixpeq2dva 8906 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
103102eqeq2d 2744 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ↔ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)))
104100, 103anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)) ↔ (((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))))
105104spcegv 3588 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) ∈ V β†’ ((((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ)) Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((π‘β€˜π‘›)(ballβ€˜((distβ€˜(π‘…β€˜π‘›)) β†Ύ ((Baseβ€˜(π‘…β€˜π‘›)) Γ— (Baseβ€˜(π‘…β€˜π‘›)))))π‘Ÿ))β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
1061053impib 1117 . . . . . . . . . . . . . . . . 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 1376 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) ∧ 0 < π‘Ÿ) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
1081073expia 1122 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ (0 < π‘Ÿ β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
10924, 108sylbid 239 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
110109adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ ((𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
111 simpr 486 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ))
112111neeq1d 3001 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (π‘₯ β‰  βˆ… ↔ (𝑝(ballβ€˜π·)π‘Ÿ) β‰  βˆ…))
113 df-3an 1090 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)))
114 ral0 4513 . . . . . . . . . . . . . . . . . . 19 βˆ€π‘˜ ∈ βˆ… (π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)
115 difeq2 4117 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝐼 β†’ (𝐼 βˆ– 𝑧) = (𝐼 βˆ– 𝐼))
116 difid 4371 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼 βˆ– 𝐼) = βˆ…
117115, 116eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝐼 β†’ (𝐼 βˆ– 𝑧) = βˆ…)
118117raleqdv 3326 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝐼 β†’ (βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜) ↔ βˆ€π‘˜ ∈ βˆ… (π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)))
119118rspcev 3613 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ Fin ∧ βˆ€π‘˜ ∈ βˆ… (π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) β†’ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
1201, 114, 119sylancl 587 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
121120adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
122121biantrud 533 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))))
123113, 122bitr4id 290 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ↔ (𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜))))
124 eqeq1 2737 . . . . . . . . . . . . . . 15 (π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ↔ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
125123, 124bi2anan9 638 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
126125exbidv 1925 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)) ↔ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
127110, 112, 1263imtr4d 294 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) ∧ π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (π‘₯ β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
128127ex 414 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*)) β†’ (π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (π‘₯ β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
129128rexlimdvva 3212 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘ ∈ 𝐡 βˆƒπ‘Ÿ ∈ ℝ* π‘₯ = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (π‘₯ β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
13019, 129sylbid 239 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ ran (ballβ€˜π·) β†’ (π‘₯ β‰  βˆ… β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
131130impd 412 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ ran (ballβ€˜π·) ∧ π‘₯ β‰  βˆ…) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
13212, 131biimtrid 241 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (ran (ballβ€˜π·) βˆ– {βˆ…}) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
133132alrimiv 1931 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯(π‘₯ ∈ (ran (ballβ€˜π·) βˆ– {βˆ…}) β†’ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘”β€˜π‘˜) ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘˜ ∈ (𝐼 βˆ– 𝑧)(π‘”β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜)) ∧ π‘₯ = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
134 ssab 4059 . . . . . 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 4034 . . . 4 (πœ‘ β†’ (ran (ballβ€˜π·) βˆ– {βˆ…}) βŠ† 𝐢)
137 ssv 4007 . . . . . . . . . 10 ∞MetSp βŠ† V
138 fnssres 6674 . . . . . . . . . 10 ((TopOpen Fn V ∧ ∞MetSp βŠ† V) β†’ (TopOpen β†Ύ ∞MetSp) Fn ∞MetSp)
1392, 137, 138mp2an 691 . . . . . . . . 9 (TopOpen β†Ύ ∞MetSp) Fn ∞MetSp
140 fvres 6911 . . . . . . . . . . 11 (π‘₯ ∈ ∞MetSp β†’ ((TopOpen β†Ύ ∞MetSp)β€˜π‘₯) = (TopOpenβ€˜π‘₯))
141 xmstps 23959 . . . . . . . . . . . 12 (π‘₯ ∈ ∞MetSp β†’ π‘₯ ∈ TopSp)
142 eqid 2733 . . . . . . . . . . . . 13 (TopOpenβ€˜π‘₯) = (TopOpenβ€˜π‘₯)
143142tpstop 22439 . . . . . . . . . . . 12 (π‘₯ ∈ TopSp β†’ (TopOpenβ€˜π‘₯) ∈ Top)
144141, 143syl 17 . . . . . . . . . . 11 (π‘₯ ∈ ∞MetSp β†’ (TopOpenβ€˜π‘₯) ∈ Top)
145140, 144eqeltrd 2834 . . . . . . . . . 10 (π‘₯ ∈ ∞MetSp β†’ ((TopOpen β†Ύ ∞MetSp)β€˜π‘₯) ∈ Top)
146145rgen 3064 . . . . . . . . 9 βˆ€π‘₯ ∈ ∞MetSp ((TopOpen β†Ύ ∞MetSp)β€˜π‘₯) ∈ Top
147 ffnfv 7118 . . . . . . . . 9 ((TopOpen β†Ύ ∞MetSp):∞MetSp⟢Top ↔ ((TopOpen β†Ύ ∞MetSp) Fn ∞MetSp ∧ βˆ€π‘₯ ∈ ∞MetSp ((TopOpen β†Ύ ∞MetSp)β€˜π‘₯) ∈ Top))
148139, 146, 147mpbir2an 710 . . . . . . . 8 (TopOpen β†Ύ ∞MetSp):∞MetSp⟢Top
149 fco2 6745 . . . . . . . 8 (((TopOpen β†Ύ ∞MetSp):∞MetSp⟢Top ∧ 𝑅:𝐼⟢∞MetSp) β†’ (TopOpen ∘ 𝑅):𝐼⟢Top)
150148, 3, 149sylancr 588 . . . . . . 7 (πœ‘ β†’ (TopOpen ∘ 𝑅):𝐼⟢Top)
151 eqid 2733 . . . . . . . 8 X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) = X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)
1529, 151ptbasfi 23085 . . . . . . 7 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅):𝐼⟢Top) β†’ 𝐢 = (fiβ€˜({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)))))
1531, 150, 152syl2anc 585 . . . . . 6 (πœ‘ β†’ 𝐢 = (fiβ€˜({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)))))
154 eqid 2733 . . . . . . . . 9 (MetOpenβ€˜π·) = (MetOpenβ€˜π·)
155154mopntop 23946 . . . . . . . 8 (𝐷 ∈ (∞Metβ€˜π΅) β†’ (MetOpenβ€˜π·) ∈ Top)
15617, 155syl 17 . . . . . . 7 (πœ‘ β†’ (MetOpenβ€˜π·) ∈ Top)
15713, 16, 14, 1, 4prdsbas2 17415 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 = Xπ‘˜ ∈ 𝐼 (Baseβ€˜(π‘…β€˜π‘˜)))
1583, 71sylan 581 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = 𝐾)
1593ffvelcdmda 7087 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘…β€˜π‘˜) ∈ ∞MetSp)
160 xmstps 23959 . . . . . . . . . . . . . . . . . 18 ((π‘…β€˜π‘˜) ∈ ∞MetSp β†’ (π‘…β€˜π‘˜) ∈ TopSp)
161159, 160syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘…β€˜π‘˜) ∈ TopSp)
16234, 70istps 22436 . . . . . . . . . . . . . . . . 17 ((π‘…β€˜π‘˜) ∈ TopSp ↔ 𝐾 ∈ (TopOnβ€˜π‘‰))
163161, 162sylib 217 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐾 ∈ (TopOnβ€˜π‘‰))
164158, 163eqeltrd 2834 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) ∈ (TopOnβ€˜π‘‰))
165 toponuni 22416 . . . . . . . . . . . . . . 15 (((TopOpen ∘ 𝑅)β€˜π‘˜) ∈ (TopOnβ€˜π‘‰) β†’ 𝑉 = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
166164, 165syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝑉 = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
16734, 166eqtr3id 2787 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (Baseβ€˜(π‘…β€˜π‘˜)) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
168167ixpeq2dva 8906 . . . . . . . . . . . 12 (πœ‘ β†’ Xπ‘˜ ∈ 𝐼 (Baseβ€˜(π‘…β€˜π‘˜)) = Xπ‘˜ ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
169157, 168eqtrd 2773 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 = Xπ‘˜ ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜))
170 fveq2 6892 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = ((TopOpen ∘ 𝑅)β€˜π‘›))
171170unieqd 4923 . . . . . . . . . . . 12 (π‘˜ = 𝑛 β†’ βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜) = βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›))
172171cbvixpv 8909 . . . . . . . . . . 11 Xπ‘˜ ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘˜) = X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)
173169, 172eqtrdi 2789 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 = X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›))
174154mopntopon 23945 . . . . . . . . . . . 12 (𝐷 ∈ (∞Metβ€˜π΅) β†’ (MetOpenβ€˜π·) ∈ (TopOnβ€˜π΅))
17517, 174syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (MetOpenβ€˜π·) ∈ (TopOnβ€˜π΅))
176 toponmax 22428 . . . . . . . . . . 11 ((MetOpenβ€˜π·) ∈ (TopOnβ€˜π΅) β†’ 𝐡 ∈ (MetOpenβ€˜π·))
177175, 176syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ (MetOpenβ€˜π·))
178173, 177eqeltrrd 2835 . . . . . . . . 9 (πœ‘ β†’ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ∈ (MetOpenβ€˜π·))
179178snssd 4813 . . . . . . . 8 (πœ‘ β†’ {X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βŠ† (MetOpenβ€˜π·))
180173mpteq1d 5244 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)))
181180ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)))
182181cnveqd 5876 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) = β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)))
183182imaeq1d 6059 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
184 fveq1 6891 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = 𝑝 β†’ (π‘€β€˜π‘˜) = (π‘β€˜π‘˜))
185184eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑀 = 𝑝 β†’ ((π‘€β€˜π‘˜) ∈ 𝑒 ↔ (π‘β€˜π‘˜) ∈ 𝑒))
186 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜))
187186mptpreima 6238 . . . . . . . . . . . . . . . . . . 19 (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = {𝑀 ∈ 𝐡 ∣ (π‘€β€˜π‘˜) ∈ 𝑒}
188185, 187elrab2 3687 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))
189159, 36syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐸 ∈ (∞Metβ€˜π‘‰))
190189adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝐸 ∈ (∞Metβ€˜π‘‰))
191 simprl 770 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝑒 ∈ 𝐾)
192159, 73syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐾 = (MetOpenβ€˜πΈ))
193192adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝐾 = (MetOpenβ€˜πΈ))
194191, 193eleqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝑒 ∈ (MetOpenβ€˜πΈ))
195 simprrr 781 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ (π‘β€˜π‘˜) ∈ 𝑒)
19653mopni2 24002 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Metβ€˜π‘‰) ∧ 𝑒 ∈ (MetOpenβ€˜πΈ) ∧ (π‘β€˜π‘˜) ∈ 𝑒) β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)
197190, 194, 195, 196syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)
19817ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ 𝐷 ∈ (∞Metβ€˜π΅))
199 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ 𝑝 ∈ 𝐡)
200199adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ 𝑝 ∈ 𝐡)
201 rpxr 12983 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ*)
202201ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ π‘Ÿ ∈ ℝ*)
203154blopn 24009 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Metβ€˜π΅) ∧ 𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) ∈ (MetOpenβ€˜π·))
204198, 200, 202, 203syl3anc 1372 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) ∈ (MetOpenβ€˜π·))
205 simprl 770 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ π‘Ÿ ∈ ℝ+)
206 blcntr 23919 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Metβ€˜π΅) ∧ 𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ))
207198, 200, 205, 206syl3anc 1372 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ 𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ))
208 blssm 23924 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (∞Metβ€˜π΅) ∧ 𝑝 ∈ 𝐡 ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† 𝐡)
209198, 200, 202, 208syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† 𝐡)
210 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)
211 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ πœ‘)
212 rpgt0 12986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (π‘Ÿ ∈ ℝ+ β†’ 0 < π‘Ÿ)
213212ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ 0 < π‘Ÿ)
214211, 200, 202, 213, 95syl121anc 1376 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) = Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
215214eleq2d 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ) ↔ 𝑀 ∈ Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)))
216215biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ 𝑀 ∈ Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
217 vex 3479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑀 ∈ V
218217elixp 8898 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) ↔ (𝑀 Fn 𝐼 ∧ βˆ€π‘˜ ∈ 𝐼 (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)))
219218simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 ∈ Xπ‘˜ ∈ 𝐼 ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) β†’ βˆ€π‘˜ ∈ 𝐼 (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
220216, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ βˆ€π‘˜ ∈ 𝐼 (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
221 simp-4r 783 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ π‘˜ ∈ 𝐼)
222 rsp 3245 . . . . . . . . . . . . . . . . . . . . . . . . 25 (βˆ€π‘˜ ∈ 𝐼 (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) β†’ (π‘˜ ∈ 𝐼 β†’ (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ)))
223220, 221, 222sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (π‘€β€˜π‘˜) ∈ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ))
224210, 223sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) ∧ 𝑀 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)) β†’ (π‘€β€˜π‘˜) ∈ 𝑒)
225209, 224ssrabdv 4072 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† {𝑀 ∈ 𝐡 ∣ (π‘€β€˜π‘˜) ∈ 𝑒})
226225, 187sseqtrrdi 4034 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))
227 eleq2 2823 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (𝑝 ∈ 𝑦 ↔ 𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ)))
228 sseq1 4008 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ (𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ↔ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
229227, 228anbi12d 632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑝(ballβ€˜π·)π‘Ÿ) β†’ ((𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)) ↔ (𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
230229rspcev 3613 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝(ballβ€˜π·)π‘Ÿ) ∈ (MetOpenβ€˜π·) ∧ (𝑝 ∈ (𝑝(ballβ€˜π·)π‘Ÿ) ∧ (𝑝(ballβ€˜π·)π‘Ÿ) βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
231204, 207, 226, 230syl12anc 836 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ ((π‘β€˜π‘˜)(ballβ€˜πΈ)π‘Ÿ) βŠ† 𝑒)) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
232197, 231rexlimddv 3162 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ (𝑒 ∈ 𝐾 ∧ (𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒))) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
233232expr 458 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ ((𝑝 ∈ 𝐡 ∧ (π‘β€˜π‘˜) ∈ 𝑒) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
234188, 233biimtrid 241 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (𝑝 ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) β†’ βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
235234ralrimiv 3146 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ βˆ€π‘ ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)))
236156ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (MetOpenβ€˜π·) ∈ Top)
237 eltop2 22478 . . . . . . . . . . . . . . . . 17 ((MetOpenβ€˜π·) ∈ Top β†’ ((β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘ ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
238236, 237syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ ((β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘ ∈ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒)βˆƒπ‘¦ ∈ (MetOpenβ€˜π·)(𝑝 ∈ 𝑦 ∧ 𝑦 βŠ† (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒))))
239235, 238mpbird 257 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑀 ∈ 𝐡 ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
240183, 239eqeltrrd 2835 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ 𝑒 ∈ 𝐾) β†’ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
241240ralrimiva 3147 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘’ ∈ 𝐾 (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
242158raleqdv 3326 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘’ ∈ 𝐾 (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·)))
243241, 242mpbird 257 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
244243ralrimiva 3147 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
245 fveq2 6892 . . . . . . . . . . . . 13 (π‘˜ = π‘š β†’ ((TopOpen ∘ 𝑅)β€˜π‘˜) = ((TopOpen ∘ 𝑅)β€˜π‘š))
246 fveq2 6892 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘š β†’ (π‘€β€˜π‘˜) = (π‘€β€˜π‘š))
247246mpteq2dv 5251 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘š β†’ (𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = (𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)))
248247cnveqd 5876 . . . . . . . . . . . . . . 15 (π‘˜ = π‘š β†’ β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) = β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)))
249248imaeq1d 6059 . . . . . . . . . . . . . 14 (π‘˜ = π‘š β†’ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) = (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒))
250249eleq1d 2819 . . . . . . . . . . . . 13 (π‘˜ = π‘š β†’ ((β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·)))
251245, 250raleqbidv 3343 . . . . . . . . . . . 12 (π‘˜ = π‘š β†’ (βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘š)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·)))
252251cbvralvw 3235 . . . . . . . . . . 11 (βˆ€π‘˜ ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘˜)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘˜)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ βˆ€π‘š ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘š)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
253244, 252sylib 217 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘š ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘š)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·))
254 eqid 2733 . . . . . . . . . . 11 (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)) = (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒))
255254fmpox 8053 . . . . . . . . . 10 (βˆ€π‘š ∈ 𝐼 βˆ€π‘’ ∈ ((TopOpen ∘ 𝑅)β€˜π‘š)(β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒) ∈ (MetOpenβ€˜π·) ↔ (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)):βˆͺ π‘š ∈ 𝐼 ({π‘š} Γ— ((TopOpen ∘ 𝑅)β€˜π‘š))⟢(MetOpenβ€˜π·))
256253, 255sylib 217 . . . . . . . . 9 (πœ‘ β†’ (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)):βˆͺ π‘š ∈ 𝐼 ({π‘š} Γ— ((TopOpen ∘ 𝑅)β€˜π‘š))⟢(MetOpenβ€˜π·))
257256frnd 6726 . . . . . . . 8 (πœ‘ β†’ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)) βŠ† (MetOpenβ€˜π·))
258179, 257unssd 4187 . . . . . . 7 (πœ‘ β†’ ({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒))) βŠ† (MetOpenβ€˜π·))
259 fiss 9419 . . . . . . 7 (((MetOpenβ€˜π·) ∈ Top ∧ ({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒))) βŠ† (MetOpenβ€˜π·)) β†’ (fiβ€˜({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)))) βŠ† (fiβ€˜(MetOpenβ€˜π·)))
260156, 258, 259syl2anc 585 . . . . . 6 (πœ‘ β†’ (fiβ€˜({X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›)} βˆͺ ran (π‘š ∈ 𝐼, 𝑒 ∈ ((TopOpen ∘ 𝑅)β€˜π‘š) ↦ (β—‘(𝑀 ∈ X𝑛 ∈ 𝐼 βˆͺ ((TopOpen ∘ 𝑅)β€˜π‘›) ↦ (π‘€β€˜π‘š)) β€œ 𝑒)))) βŠ† (fiβ€˜(MetOpenβ€˜π·)))
261153, 260eqsstrd 4021 . . . . 5 (πœ‘ β†’ 𝐢 βŠ† (fiβ€˜(MetOpenβ€˜π·)))
262 fitop 22402 . . . . . . 7 ((MetOpenβ€˜π·) ∈ Top β†’ (fiβ€˜(MetOpenβ€˜π·)) = (MetOpenβ€˜π·))
263156, 262syl 17 . . . . . 6 (πœ‘ β†’ (fiβ€˜(MetOpenβ€˜π·)) = (MetOpenβ€˜π·))
264154mopnval 23944 . . . . . . . 8 (𝐷 ∈ (∞Metβ€˜π΅) β†’ (MetOpenβ€˜π·) = (topGenβ€˜ran (ballβ€˜π·)))
26517, 264syl 17 . . . . . . 7 (πœ‘ β†’ (MetOpenβ€˜π·) = (topGenβ€˜ran (ballβ€˜π·)))
266 tgdif0 22495 . . . . . . 7 (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})) = (topGenβ€˜ran (ballβ€˜π·))
267265, 266eqtr4di 2791 . . . . . 6 (πœ‘ β†’ (MetOpenβ€˜π·) = (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})))
268263, 267eqtrd 2773 . . . . 5 (πœ‘ β†’ (fiβ€˜(MetOpenβ€˜π·)) = (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})))
269261, 268sseqtrd 4023 . . . 4 (πœ‘ β†’ 𝐢 βŠ† (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})))
270 2basgen 22493 . . . 4 (((ran (ballβ€˜π·) βˆ– {βˆ…}) βŠ† 𝐢 ∧ 𝐢 βŠ† (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…}))) β†’ (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})) = (topGenβ€˜πΆ))
271136, 269, 270syl2anc 585 . . 3 (πœ‘ β†’ (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})) = (topGenβ€˜πΆ))
27211, 271eqtr4d 2776 . 2 (πœ‘ β†’ (∏tβ€˜(TopOpen ∘ 𝑅)) = (topGenβ€˜(ran (ballβ€˜π·) βˆ– {βˆ…})))
273 prdsxms.j . . 3 𝐽 = (TopOpenβ€˜π‘Œ)
27413, 14, 1, 4, 273prdstopn 23132 . 2 (πœ‘ β†’ 𝐽 = (∏tβ€˜(TopOpen ∘ 𝑅)))
275272, 274, 2673eqtr4d 2783 1 (πœ‘ β†’ 𝐽 = (MetOpenβ€˜π·))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   βŠ† wss 3949  βˆ…c0 4323  {csn 4629  βˆͺ cuni 4909  βˆͺ ciun 4998   class class class wbr 5149   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680   ∘ ccom 5681   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  Xcixp 8891  Fincfn 8939  ficfi 9405  0cc0 11110  β„*cxr 11247   < clt 11248  β„+crp 12974  Basecbs 17144  distcds 17206  TopOpenctopn 17367  topGenctg 17383  βˆtcpt 17384  Xscprds 17391  βˆžMetcxmet 20929  ballcbl 20931  MetOpencmopn 20934  Topctop 22395  TopOnctopon 22412  TopSpctps 22434  βˆžMetSpcxms 23823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fi 9406  df-sup 9437  df-inf 9438  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-icc 13331  df-fz 13485  df-struct 17080  df-slot 17115  df-ndx 17127  df-base 17145  df-plusg 17210  df-mulr 17211  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-hom 17221  df-cco 17222  df-rest 17368  df-topn 17369  df-topgen 17389  df-pt 17390  df-prds 17393  df-psmet 20936  df-xmet 20937  df-bl 20939  df-mopn 20940  df-top 22396  df-topon 22413  df-topsp 22435  df-bases 22449  df-xms 23826
This theorem is referenced by:  prdsxms  24039
  Copyright terms: Public domain W3C validator