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

Theorem prdsxmslem2 22381
Description: Lemma for prdsxms 22382. 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 16133 . . . . 5 TopOpen Fn V
3 prdsxms.r . . . . . . 7 (𝜑𝑅:𝐼⟶∞MetSp)
4 ffn 6083 . . . . . . 7 (𝑅:𝐼⟶∞MetSp → 𝑅 Fn 𝐼)
53, 4syl 17 . . . . . 6 (𝜑𝑅 Fn 𝐼)
6 dffn2 6085 . . . . . 6 (𝑅 Fn 𝐼𝑅:𝐼⟶V)
75, 6sylib 208 . . . . 5 (𝜑𝑅:𝐼⟶V)
8 fnfco 6107 . . . . 5 ((TopOpen Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen ∘ 𝑅) Fn 𝐼)
92, 7, 8sylancr 696 . . . 4 (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼)
10 prdsxms.c . . . . 5 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))}
1110ptval 21421 . . . 4 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
121, 9, 11syl2anc 694 . . 3 (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
13 eldifsn 4350 . . . . . . . 8 (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) ↔ (𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅))
14 prdsxms.y . . . . . . . . . . . 12 𝑌 = (𝑆Xs𝑅)
15 prdsxms.s . . . . . . . . . . . 12 (𝜑𝑆𝑊)
16 prdsxms.d . . . . . . . . . . . 12 𝐷 = (dist‘𝑌)
17 prdsxms.b . . . . . . . . . . . 12 𝐵 = (Base‘𝑌)
1814, 15, 1, 16, 17, 3prdsxmslem1 22380 . . . . . . . . . . 11 (𝜑𝐷 ∈ (∞Met‘𝐵))
19 blrn 22261 . . . . . . . . . . 11 (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
2018, 19syl 17 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
2118adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵))
22 simprl 809 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝑝𝐵)
23 simprr 811 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝑟 ∈ ℝ*)
24 xbln0 22266 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
2521, 22, 23, 24syl3anc 1366 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
2613ad2ant1 1102 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐼 ∈ Fin)
27 mptexg 6525 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ Fin → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V)
2826, 27syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V)
29 ovex 6718 . . . . . . . . . . . . . . . . . . 19 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V
3029rgenw 2953 . . . . . . . . . . . . . . . . . 18 𝑛𝐼 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V
31 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))
3231fnmpt 6058 . . . . . . . . . . . . . . . . . 18 (∀𝑛𝐼 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼)
3330, 32mp1i 13 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼)
3433ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅:𝐼⟶∞MetSp)
3534ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → (𝑅𝑘) ∈ ∞MetSp)
36 prdsxms.v . . . . . . . . . . . . . . . . . . . . . 22 𝑉 = (Base‘(𝑅𝑘))
37 prdsxms.e . . . . . . . . . . . . . . . . . . . . . 22 𝐸 = ((dist‘(𝑅𝑘)) ↾ (𝑉 × 𝑉))
3836, 37xmsxmet 22308 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉))
3935, 38syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝐸 ∈ (∞Met‘𝑉))
40 eqid 2651 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))
41 eqid 2651 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))) = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
42153ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑆𝑊)
4335ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 (𝑅𝑘) ∈ ∞MetSp)
44 simp2l 1107 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝𝐵)
4534feqmptd 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑘𝐼 ↦ (𝑅𝑘)))
4645oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
4714, 46syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
4847fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
4917, 48syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
5044, 49eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
5140, 41, 42, 26, 43, 36, 50prdsbascl 16190 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 (𝑝𝑘) ∈ 𝑉)
5251r19.21bi 2961 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → (𝑝𝑘) ∈ 𝑉)
53 simp2r 1108 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑟 ∈ ℝ*)
5453adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝑟 ∈ ℝ*)
55 eqid 2651 . . . . . . . . . . . . . . . . . . . . 21 (MetOpen‘𝐸) = (MetOpen‘𝐸)
5655blopn 22352 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝𝑘) ∈ 𝑉𝑟 ∈ ℝ*) → ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
5739, 52, 54, 56syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
58 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑘 → (𝑅𝑛) = (𝑅𝑘))
5958fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → (dist‘(𝑅𝑛)) = (dist‘(𝑅𝑘)))
6058fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → (Base‘(𝑅𝑛)) = (Base‘(𝑅𝑘)))
6160, 36syl6eqr 2703 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑘 → (Base‘(𝑅𝑛)) = 𝑉)
6261sqxpeqd 5175 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛))) = (𝑉 × 𝑉))
6359, 62reseq12d 5429 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → ((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))) = ((dist‘(𝑅𝑘)) ↾ (𝑉 × 𝑉)))
6463, 37syl6eqr 2703 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → ((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))) = 𝐸)
6564fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛))))) = (ball‘𝐸))
66 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (𝑝𝑛) = (𝑝𝑘))
67 eqidd 2652 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘𝑟 = 𝑟)
6865, 66, 67oveq123d 6711 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) = ((𝑝𝑘)(ball‘𝐸)𝑟))
69 ovex 6718 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ V
7068, 31, 69fvmpt 6321 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝐼 → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
7170adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
72 fvco3 6314 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅:𝐼⟶∞MetSp ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅𝑘)))
73 prdsxms.k . . . . . . . . . . . . . . . . . . . . . 22 𝐾 = (TopOpen‘(𝑅𝑘))
7472, 73syl6eqr 2703 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅:𝐼⟶∞MetSp ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
7534, 74sylan 487 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
7673, 36, 37xmstopn 22303 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸))
7735, 76syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝐾 = (MetOpen‘𝐸))
7875, 77eqtrd 2685 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸))
7957, 71, 783eltr4d 2745 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
8079ralrimiva 2995 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
8134feqmptd 6288 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑛𝐼 ↦ (𝑅𝑛)))
8281oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
8314, 82syl5eq 2697 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
8483fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
8516, 84syl5eq 2697 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
8685fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))))
8786oveqd 6707 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))𝑟))
8858cbvmptv 4783 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐼 ↦ (𝑅𝑛)) = (𝑘𝐼 ↦ (𝑅𝑘))
8988oveq2i 6701 . . . . . . . . . . . . . . . . . . 19 (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))
90 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))) = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
91 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))) = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
9283fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
9317, 92syl5eq 2697 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
9444, 93eleqtrd 2732 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
95 simp3 1083 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 0 < 𝑟)
9689, 90, 36, 37, 91, 42, 26, 35, 39, 94, 53, 95prdsbl 22343 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
9787, 96eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
98 fneq1 6017 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (𝑔 Fn 𝐼 ↔ (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼))
99 fveq1 6228 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (𝑔𝑘) = ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘))
10099eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
101100ralbidv 3015 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
10298, 101anbi12d 747 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
10399, 70sylan9eq 2705 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∧ 𝑘𝐼) → (𝑔𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
104103ixpeq2dva 7965 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → X𝑘𝐼 (𝑔𝑘) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
105104eqeq2d 2661 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)))
106102, 105anbi12d 747 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)) ↔ (((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))))
107106spcegv 3325 . . . . . . . . . . . . . . . . . 18 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V → ((((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
1081073impib 1281 . . . . . . . . . . . . . . . . 17 (((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V ∧ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
10928, 33, 80, 97, 108syl121anc 1371 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
1101093expia 1286 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → (0 < 𝑟 → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
11125, 110sylbid 230 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
112111adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
113 simpr 476 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → 𝑥 = (𝑝(ball‘𝐷)𝑟))
114113neeq1d 2882 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ ↔ (𝑝(ball‘𝐷)𝑟) ≠ ∅))
115 ral0 4109 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)
116 difeq2 3755 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝐼 → (𝐼𝑧) = (𝐼𝐼))
117 difid 3981 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝐼) = ∅
118116, 117syl6eq 2701 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝐼 → (𝐼𝑧) = ∅)
119118raleqdv 3174 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)))
120119rspcev 3340 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ Fin ∧ ∀𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
1211, 115, 120sylancl 695 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
122121adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
123122biantrud 527 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))))
124 df-3an 1056 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)))
125123, 124syl6rbbr 279 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
126 eqeq1 2655 . . . . . . . . . . . . . . 15 (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘𝐼 (𝑔𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
127125, 126bi2anan9 935 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
128127exbidv 1890 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
129112, 114, 1283imtr4d 283 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
130129ex 449 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
131130rexlimdvva 3067 . . . . . . . . . 10 (𝜑 → (∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
13220, 131sylbid 230 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ran (ball‘𝐷) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
133132impd 446 . . . . . . . 8 (𝜑 → ((𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
13413, 133syl5bi 232 . . . . . . 7 (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
135134alrimiv 1895 . . . . . 6 (𝜑 → ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
136 ssab 3705 . . . . . 6 ((ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))} ↔ ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
137135, 136sylibr 224 . . . . 5 (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))})
138137, 10syl6sseqr 3685 . . . 4 (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶)
139 ssv 3658 . . . . . . . . . 10 ∞MetSp ⊆ V
140 fnssres 6042 . . . . . . . . . 10 ((TopOpen Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn ∞MetSp)
1412, 139, 140mp2an 708 . . . . . . . . 9 (TopOpen ↾ ∞MetSp) Fn ∞MetSp
142 fvres 6245 . . . . . . . . . . 11 (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) = (TopOpen‘𝑥))
143 xmstps 22305 . . . . . . . . . . . 12 (𝑥 ∈ ∞MetSp → 𝑥 ∈ TopSp)
144 eqid 2651 . . . . . . . . . . . . 13 (TopOpen‘𝑥) = (TopOpen‘𝑥)
145144tpstop 20789 . . . . . . . . . . . 12 (𝑥 ∈ TopSp → (TopOpen‘𝑥) ∈ Top)
146143, 145syl 17 . . . . . . . . . . 11 (𝑥 ∈ ∞MetSp → (TopOpen‘𝑥) ∈ Top)
147142, 146eqeltrd 2730 . . . . . . . . . 10 (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top)
148147rgen 2951 . . . . . . . . 9 𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top
149 ffnfv 6428 . . . . . . . . 9 ((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ↔ ((TopOpen ↾ ∞MetSp) Fn ∞MetSp ∧ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top))
150141, 148, 149mpbir2an 975 . . . . . . . 8 (TopOpen ↾ ∞MetSp):∞MetSp⟶Top
151 fco2 6097 . . . . . . . 8 (((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen ∘ 𝑅):𝐼⟶Top)
152150, 3, 151sylancr 696 . . . . . . 7 (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top)
153 eqid 2651 . . . . . . . 8 X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)
15410, 153ptbasfi 21432 . . . . . . 7 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅):𝐼⟶Top) → 𝐶 = (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))))
1551, 152, 154syl2anc 694 . . . . . 6 (𝜑𝐶 = (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))))
156 eqid 2651 . . . . . . . . 9 (MetOpen‘𝐷) = (MetOpen‘𝐷)
157156mopntop 22292 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top)
15818, 157syl 17 . . . . . . 7 (𝜑 → (MetOpen‘𝐷) ∈ Top)
15914, 17, 15, 1, 5prdsbas2 16176 . . . . . . . . . . . 12 (𝜑𝐵 = X𝑘𝐼 (Base‘(𝑅𝑘)))
1603, 74sylan 487 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
1613ffvelrnda 6399 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → (𝑅𝑘) ∈ ∞MetSp)
162 xmstps 22305 . . . . . . . . . . . . . . . . . 18 ((𝑅𝑘) ∈ ∞MetSp → (𝑅𝑘) ∈ TopSp)
163161, 162syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑅𝑘) ∈ TopSp)
16436, 73istps 20786 . . . . . . . . . . . . . . . . 17 ((𝑅𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉))
165163, 164sylib 208 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → 𝐾 ∈ (TopOn‘𝑉))
166160, 165eqeltrd 2730 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉))
167 toponuni 20767 . . . . . . . . . . . . . . 15 (((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ((TopOpen ∘ 𝑅)‘𝑘))
168166, 167syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐼) → 𝑉 = ((TopOpen ∘ 𝑅)‘𝑘))
16936, 168syl5eqr 2699 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (Base‘(𝑅𝑘)) = ((TopOpen ∘ 𝑅)‘𝑘))
170169ixpeq2dva 7965 . . . . . . . . . . . 12 (𝜑X𝑘𝐼 (Base‘(𝑅𝑘)) = X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘))
171159, 170eqtrd 2685 . . . . . . . . . . 11 (𝜑𝐵 = X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘))
172 fveq2 6229 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
173172unieqd 4478 . . . . . . . . . . . 12 (𝑘 = 𝑛 ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
174173cbvixpv 7968 . . . . . . . . . . 11 X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)
175171, 174syl6eq 2701 . . . . . . . . . 10 (𝜑𝐵 = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛))
176156mopntopon 22291 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
17718, 176syl 17 . . . . . . . . . . 11 (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
178 toponmax 20778 . . . . . . . . . . 11 ((MetOpen‘𝐷) ∈ (TopOn‘𝐵) → 𝐵 ∈ (MetOpen‘𝐷))
179177, 178syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ (MetOpen‘𝐷))
180175, 179eqeltrrd 2731 . . . . . . . . 9 (𝜑X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷))
181180snssd 4372 . . . . . . . 8 (𝜑 → {X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷))
182175mpteq1d 4771 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
183182ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
184183cnveqd 5330 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
185184imaeq1d 5500 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢))
186 fveq1 6228 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑝 → (𝑤𝑘) = (𝑝𝑘))
187186eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑝 → ((𝑤𝑘) ∈ 𝑢 ↔ (𝑝𝑘) ∈ 𝑢))
188 eqid 2651 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤𝐵 ↦ (𝑤𝑘))
189188mptpreima 5666 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) = {𝑤𝐵 ∣ (𝑤𝑘) ∈ 𝑢}
190187, 189elrab2 3399 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))
191161, 38syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝐼) → 𝐸 ∈ (∞Met‘𝑉))
192191adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉))
193 simprl 809 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑢𝐾)
194161, 76syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝐼) → 𝐾 = (MetOpen‘𝐸))
195194adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸))
196193, 195eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸))
197 simprrr 822 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → (𝑝𝑘) ∈ 𝑢)
19855mopni2 22345 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
199192, 196, 197, 198syl3anc 1366 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
20018ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵))
201 simprrl 821 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑝𝐵)
202201adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝𝐵)
203 rpxr 11878 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
204203ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*)
205156blopn 22352 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
206200, 202, 204, 205syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
207 simprl 809 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
208 blcntr 22265 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
209200, 202, 207, 208syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
210 blssm 22270 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
211200, 202, 204, 210syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
212 simplrr 818 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
213 simplll 813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑)
214 rpgt0 11882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑟 ∈ ℝ+ → 0 < 𝑟)
215214ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟)
216213, 202, 204, 215, 97syl121anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
217216eleq2d 2716 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)))
218217biimpa 500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
219 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑤 ∈ V
220219elixp 7957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟) ↔ (𝑤 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟)))
221220simprbi 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟) → ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
222218, 221syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
223 simp-4r 824 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘𝐼)
224 rsp 2958 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟) → (𝑘𝐼 → (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟)))
225222, 223, 224sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
226212, 225sseldd 3637 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤𝑘) ∈ 𝑢)
227211, 226ssrabdv 3714 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤𝐵 ∣ (𝑤𝑘) ∈ 𝑢})
228227, 189syl6sseqr 3685 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))
229 eleq2 2719 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝𝑦𝑝 ∈ (𝑝(ball‘𝐷)𝑟)))
230 sseq1 3659 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
231229, 230anbi12d 747 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
232231rspcev 3340 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
233206, 209, 228, 232syl12anc 1364 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
234199, 233rexlimddv 3064 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
235234expr 642 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
236190, 235syl5bi 232 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
237236ralrimiv 2994 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
238158ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (MetOpen‘𝐷) ∈ Top)
239 eltop2 20827 . . . . . . . . . . . . . . . . 17 ((MetOpen‘𝐷) ∈ Top → (((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
240238, 239syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
241237, 240mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
242185, 241eqeltrrd 2731 . . . . . . . . . . . . . 14 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
243242ralrimiva 2995 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → ∀𝑢𝐾 ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
244160raleqdv 3174 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢𝐾 ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)))
245243, 244mpbird 247 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
246245ralrimiva 2995 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
247 fveq2 6229 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚))
248 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝑤𝑘) = (𝑤𝑚))
249248mpteq2dv 4778 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)))
250249cnveqd 5330 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚(𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)))
251250imaeq1d 5500 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))
252251eleq1d 2715 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → (((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
253247, 252raleqbidv 3182 . . . . . . . . . . . 12 (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
254253cbvralv 3201 . . . . . . . . . . 11 (∀𝑘𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
255246, 254sylib 208 . . . . . . . . . 10 (𝜑 → ∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
256 eqid 2651 . . . . . . . . . . 11 (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) = (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))
257256fmpt2x 7281 . . . . . . . . . 10 (∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
258255, 257sylib 208 . . . . . . . . 9 (𝜑 → (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
259 frn 6091 . . . . . . . . 9 ((𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷) → ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
260258, 259syl 17 . . . . . . . 8 (𝜑 → ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
261181, 260unssd 3822 . . . . . . 7 (𝜑 → ({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷))
262 fiss 8371 . . . . . . 7 (((MetOpen‘𝐷) ∈ Top ∧ ({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷)) → (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
263158, 261, 262syl2anc 694 . . . . . 6 (𝜑 → (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
264155, 263eqsstrd 3672 . . . . 5 (𝜑𝐶 ⊆ (fi‘(MetOpen‘𝐷)))
265 fitop 20753 . . . . . . 7 ((MetOpen‘𝐷) ∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
266158, 265syl 17 . . . . . 6 (𝜑 → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
267156mopnval 22290 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
26818, 267syl 17 . . . . . . 7 (𝜑 → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
269 tgdif0 20844 . . . . . . 7 (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran (ball‘𝐷))
270268, 269syl6eqr 2703 . . . . . 6 (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
271266, 270eqtrd 2685 . . . . 5 (𝜑 → (fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
272264, 271sseqtrd 3674 . . . 4 (𝜑𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅})))
273 2basgen 20842 . . . 4 (((ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅}))) → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
274138, 272, 273syl2anc 694 . . 3 (𝜑 → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
27512, 274eqtr4d 2688 . 2 (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
276 prdsxms.j . . 3 𝐽 = (TopOpen‘𝑌)
27714, 15, 1, 5, 276prdstopn 21479 . 2 (𝜑𝐽 = (∏t‘(TopOpen ∘ 𝑅)))
278275, 277, 2703eqtr4d 2695 1 (𝜑𝐽 = (MetOpen‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054  wal 1521   = wceq 1523  wex 1744  wcel 2030  {cab 2637  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  wss 3607  c0 3948  {csn 4210   cuni 4468   ciun 4552   class class class wbr 4685  cmpt 4762   × cxp 5141  ccnv 5142  ran crn 5144  cres 5145  cima 5146  ccom 5147   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  Xcixp 7950  Fincfn 7997  ficfi 8357  0cc0 9974  *cxr 10111   < clt 10112  +crp 11870  Basecbs 15904  distcds 15997  TopOpenctopn 16129  topGenctg 16145  tcpt 16146  Xscprds 16153  ∞Metcxmt 19779  ballcbl 19781  MetOpencmopn 19784  Topctop 20746  TopOnctopon 20763  TopSpctps 20784  ∞MetSpcxme 22169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-icc 12220  df-fz 12365  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-plusg 16001  df-mulr 16002  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-topgen 16151  df-pt 16152  df-prds 16155  df-psmet 19786  df-xmet 19787  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-xms 22172
This theorem is referenced by:  prdsxms  22382
  Copyright terms: Public domain W3C validator