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

Theorem prdsxmslem2 22613
Description: Lemma for prdsxms 22614. 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 16354 . . . . 5 TopOpen Fn V
3 prdsxms.r . . . . . . 7 (𝜑𝑅:𝐼⟶∞MetSp)
43ffnd 6224 . . . . . 6 (𝜑𝑅 Fn 𝐼)
5 dffn2 6225 . . . . . 6 (𝑅 Fn 𝐼𝑅:𝐼⟶V)
64, 5sylib 209 . . . . 5 (𝜑𝑅:𝐼⟶V)
7 fnfco 6251 . . . . 5 ((TopOpen Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen ∘ 𝑅) Fn 𝐼)
82, 6, 7sylancr 581 . . . 4 (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼)
9 prdsxms.c . . . . 5 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))}
109ptval 21653 . . . 4 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
111, 8, 10syl2anc 579 . . 3 (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
12 eldifsn 4472 . . . . . . . 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 22612 . . . . . . . . . . 11 (𝜑𝐷 ∈ (∞Met‘𝐵))
18 blrn 22493 . . . . . . . . . . 11 (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
1917, 18syl 17 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
2017adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵))
21 simprl 787 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝑝𝐵)
22 simprr 789 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝑟 ∈ ℝ*)
23 xbln0 22498 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
2420, 21, 22, 23syl3anc 1490 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
2513ad2ant1 1163 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐼 ∈ Fin)
26 mptexg 6677 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ Fin → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V)
2725, 26syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V)
28 ovex 6874 . . . . . . . . . . . . . . . . . . 19 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V
2928rgenw 3071 . . . . . . . . . . . . . . . . . 18 𝑛𝐼 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V
30 eqid 2765 . . . . . . . . . . . . . . . . . . 19 (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))
3130fnmpt 6198 . . . . . . . . . . . . . . . . . 18 (∀𝑛𝐼 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼)
3229, 31mp1i 13 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼)
3333ad2ant1 1163 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅:𝐼⟶∞MetSp)
3433ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → (𝑅𝑘) ∈ ∞MetSp)
35 prdsxms.v . . . . . . . . . . . . . . . . . . . . . 22 𝑉 = (Base‘(𝑅𝑘))
36 prdsxms.e . . . . . . . . . . . . . . . . . . . . . 22 𝐸 = ((dist‘(𝑅𝑘)) ↾ (𝑉 × 𝑉))
3735, 36xmsxmet 22540 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉))
3834, 37syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝐸 ∈ (∞Met‘𝑉))
39 eqid 2765 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))
40 eqid 2765 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))) = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
41143ad2ant1 1163 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑆𝑊)
4234ralrimiva 3113 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 (𝑅𝑘) ∈ ∞MetSp)
43 simp2l 1256 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝𝐵)
4433feqmptd 6438 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑘𝐼 ↦ (𝑅𝑘)))
4544oveq2d 6858 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
4613, 45syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
4746fveq2d 6379 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
4816, 47syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
4943, 48eleqtrd 2846 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
5039, 40, 41, 25, 42, 35, 49prdsbascl 16411 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 (𝑝𝑘) ∈ 𝑉)
5150r19.21bi 3079 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → (𝑝𝑘) ∈ 𝑉)
52 simp2r 1257 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑟 ∈ ℝ*)
5352adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝑟 ∈ ℝ*)
54 eqid 2765 . . . . . . . . . . . . . . . . . . . . 21 (MetOpen‘𝐸) = (MetOpen‘𝐸)
5554blopn 22584 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝𝑘) ∈ 𝑉𝑟 ∈ ℝ*) → ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
5638, 51, 53, 55syl3anc 1490 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
57 2fveq3 6380 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → (dist‘(𝑅𝑛)) = (dist‘(𝑅𝑘)))
58 2fveq3 6380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → (Base‘(𝑅𝑛)) = (Base‘(𝑅𝑘)))
5958, 35syl6eqr 2817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑘 → (Base‘(𝑅𝑛)) = 𝑉)
6059sqxpeqd 5309 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛))) = (𝑉 × 𝑉))
6157, 60reseq12d 5566 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → ((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))) = ((dist‘(𝑅𝑘)) ↾ (𝑉 × 𝑉)))
6261, 36syl6eqr 2817 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → ((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))) = 𝐸)
6362fveq2d 6379 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛))))) = (ball‘𝐸))
64 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (𝑝𝑛) = (𝑝𝑘))
65 eqidd 2766 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘𝑟 = 𝑟)
6663, 64, 65oveq123d 6863 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) = ((𝑝𝑘)(ball‘𝐸)𝑟))
67 ovex 6874 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ V
6866, 30, 67fvmpt 6471 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝐼 → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
6968adantl 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
70 fvco3 6464 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅:𝐼⟶∞MetSp ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅𝑘)))
71 prdsxms.k . . . . . . . . . . . . . . . . . . . . . 22 𝐾 = (TopOpen‘(𝑅𝑘))
7270, 71syl6eqr 2817 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅:𝐼⟶∞MetSp ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
7333, 72sylan 575 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
7471, 35, 36xmstopn 22535 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸))
7534, 74syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝐾 = (MetOpen‘𝐸))
7673, 75eqtrd 2799 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸))
7756, 69, 763eltr4d 2859 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
7877ralrimiva 3113 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
7933feqmptd 6438 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑛𝐼 ↦ (𝑅𝑛)))
8079oveq2d 6858 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
8113, 80syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
8281fveq2d 6379 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
8315, 82syl5eq 2811 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
8483fveq2d 6379 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))))
8584oveqd 6859 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))𝑟))
86 fveq2 6375 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → (𝑅𝑛) = (𝑅𝑘))
8786cbvmptv 4909 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐼 ↦ (𝑅𝑛)) = (𝑘𝐼 ↦ (𝑅𝑘))
8887oveq2i 6853 . . . . . . . . . . . . . . . . . . 19 (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))
89 eqid 2765 . . . . . . . . . . . . . . . . . . 19 (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))) = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
90 eqid 2765 . . . . . . . . . . . . . . . . . . 19 (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))) = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
9181fveq2d 6379 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
9216, 91syl5eq 2811 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
9343, 92eleqtrd 2846 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
94 simp3 1168 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 0 < 𝑟)
9588, 89, 35, 36, 90, 41, 25, 34, 38, 93, 52, 94prdsbl 22575 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
9685, 95eqtrd 2799 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
97 fneq1 6157 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (𝑔 Fn 𝐼 ↔ (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼))
98 fveq1 6374 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (𝑔𝑘) = ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘))
9998eleq1d 2829 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
10099ralbidv 3133 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
10197, 100anbi12d 624 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
10298, 68sylan9eq 2819 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∧ 𝑘𝐼) → (𝑔𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
103102ixpeq2dva 8128 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → X𝑘𝐼 (𝑔𝑘) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
104103eqeq2d 2775 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)))
105101, 104anbi12d 624 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)) ↔ (((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))))
106105spcegv 3446 . . . . . . . . . . . . . . . . . 18 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V → ((((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
1071063impib 1144 . . . . . . . . . . . . . . . . 17 (((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V ∧ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
10827, 32, 78, 96, 107syl121anc 1494 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
1091083expia 1150 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → (0 < 𝑟 → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
11024, 109sylbid 231 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
111110adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
112 simpr 477 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → 𝑥 = (𝑝(ball‘𝐷)𝑟))
113112neeq1d 2996 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ ↔ (𝑝(ball‘𝐷)𝑟) ≠ ∅))
114 ral0 4235 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)
115 difeq2 3884 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝐼 → (𝐼𝑧) = (𝐼𝐼))
116 difid 4113 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝐼) = ∅
117115, 116syl6eq 2815 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝐼 → (𝐼𝑧) = ∅)
118117raleqdv 3292 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)))
119118rspcev 3461 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ Fin ∧ ∀𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
1201, 114, 119sylancl 580 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
121120adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
122121biantrud 527 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))))
123 df-3an 1109 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)))
124122, 123syl6rbbr 281 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
125 eqeq1 2769 . . . . . . . . . . . . . . 15 (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘𝐼 (𝑔𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
126124, 125bi2anan9 629 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
127126exbidv 2016 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
128111, 113, 1273imtr4d 285 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
129128ex 401 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
130129rexlimdvva 3185 . . . . . . . . . 10 (𝜑 → (∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
13119, 130sylbid 231 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ran (ball‘𝐷) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
132131impd 398 . . . . . . . 8 (𝜑 → ((𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
13312, 132syl5bi 233 . . . . . . 7 (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
134133alrimiv 2022 . . . . . 6 (𝜑 → ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
135 ssab 3832 . . . . . 6 ((ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))} ↔ ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
136134, 135sylibr 225 . . . . 5 (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))})
137136, 9syl6sseqr 3812 . . . 4 (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶)
138 ssv 3785 . . . . . . . . . 10 ∞MetSp ⊆ V
139 fnssres 6182 . . . . . . . . . 10 ((TopOpen Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn ∞MetSp)
1402, 138, 139mp2an 683 . . . . . . . . 9 (TopOpen ↾ ∞MetSp) Fn ∞MetSp
141 fvres 6394 . . . . . . . . . . 11 (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) = (TopOpen‘𝑥))
142 xmstps 22537 . . . . . . . . . . . 12 (𝑥 ∈ ∞MetSp → 𝑥 ∈ TopSp)
143 eqid 2765 . . . . . . . . . . . . 13 (TopOpen‘𝑥) = (TopOpen‘𝑥)
144143tpstop 21021 . . . . . . . . . . . 12 (𝑥 ∈ TopSp → (TopOpen‘𝑥) ∈ Top)
145142, 144syl 17 . . . . . . . . . . 11 (𝑥 ∈ ∞MetSp → (TopOpen‘𝑥) ∈ Top)
146141, 145eqeltrd 2844 . . . . . . . . . 10 (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top)
147146rgen 3069 . . . . . . . . 9 𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top
148 ffnfv 6578 . . . . . . . . 9 ((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ↔ ((TopOpen ↾ ∞MetSp) Fn ∞MetSp ∧ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top))
149140, 147, 148mpbir2an 702 . . . . . . . 8 (TopOpen ↾ ∞MetSp):∞MetSp⟶Top
150 fco2 6241 . . . . . . . 8 (((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen ∘ 𝑅):𝐼⟶Top)
151149, 3, 150sylancr 581 . . . . . . 7 (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top)
152 eqid 2765 . . . . . . . 8 X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)
1539, 152ptbasfi 21664 . . . . . . 7 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅):𝐼⟶Top) → 𝐶 = (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))))
1541, 151, 153syl2anc 579 . . . . . 6 (𝜑𝐶 = (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))))
155 eqid 2765 . . . . . . . . 9 (MetOpen‘𝐷) = (MetOpen‘𝐷)
156155mopntop 22524 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top)
15717, 156syl 17 . . . . . . 7 (𝜑 → (MetOpen‘𝐷) ∈ Top)
15813, 16, 14, 1, 4prdsbas2 16397 . . . . . . . . . . . 12 (𝜑𝐵 = X𝑘𝐼 (Base‘(𝑅𝑘)))
1593, 72sylan 575 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
1603ffvelrnda 6549 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → (𝑅𝑘) ∈ ∞MetSp)
161 xmstps 22537 . . . . . . . . . . . . . . . . . 18 ((𝑅𝑘) ∈ ∞MetSp → (𝑅𝑘) ∈ TopSp)
162160, 161syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑅𝑘) ∈ TopSp)
16335, 71istps 21018 . . . . . . . . . . . . . . . . 17 ((𝑅𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉))
164162, 163sylib 209 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → 𝐾 ∈ (TopOn‘𝑉))
165159, 164eqeltrd 2844 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉))
166 toponuni 20998 . . . . . . . . . . . . . . 15 (((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ((TopOpen ∘ 𝑅)‘𝑘))
167165, 166syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐼) → 𝑉 = ((TopOpen ∘ 𝑅)‘𝑘))
16835, 167syl5eqr 2813 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (Base‘(𝑅𝑘)) = ((TopOpen ∘ 𝑅)‘𝑘))
169168ixpeq2dva 8128 . . . . . . . . . . . 12 (𝜑X𝑘𝐼 (Base‘(𝑅𝑘)) = X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘))
170158, 169eqtrd 2799 . . . . . . . . . . 11 (𝜑𝐵 = X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘))
171 fveq2 6375 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
172171unieqd 4604 . . . . . . . . . . . 12 (𝑘 = 𝑛 ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
173172cbvixpv 8131 . . . . . . . . . . 11 X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)
174170, 173syl6eq 2815 . . . . . . . . . 10 (𝜑𝐵 = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛))
175155mopntopon 22523 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
17617, 175syl 17 . . . . . . . . . . 11 (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
177 toponmax 21010 . . . . . . . . . . 11 ((MetOpen‘𝐷) ∈ (TopOn‘𝐵) → 𝐵 ∈ (MetOpen‘𝐷))
178176, 177syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ (MetOpen‘𝐷))
179174, 178eqeltrrd 2845 . . . . . . . . 9 (𝜑X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷))
180179snssd 4494 . . . . . . . 8 (𝜑 → {X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷))
181174mpteq1d 4897 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
182181ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
183182cnveqd 5466 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
184183imaeq1d 5647 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢))
185 fveq1 6374 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑝 → (𝑤𝑘) = (𝑝𝑘))
186185eleq1d 2829 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑝 → ((𝑤𝑘) ∈ 𝑢 ↔ (𝑝𝑘) ∈ 𝑢))
187 eqid 2765 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤𝐵 ↦ (𝑤𝑘))
188187mptpreima 5814 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) = {𝑤𝐵 ∣ (𝑤𝑘) ∈ 𝑢}
189186, 188elrab2 3523 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))
190160, 37syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝐼) → 𝐸 ∈ (∞Met‘𝑉))
191190adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉))
192 simprl 787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑢𝐾)
193160, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝐼) → 𝐾 = (MetOpen‘𝐸))
194193adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸))
195192, 194eleqtrd 2846 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸))
196 simprrr 800 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → (𝑝𝑘) ∈ 𝑢)
19754mopni2 22577 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
198191, 195, 196, 197syl3anc 1490 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
19917ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵))
200 simprrl 799 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑝𝐵)
201200adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝𝐵)
202 rpxr 12039 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
203202ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*)
204155blopn 22584 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
205199, 201, 203, 204syl3anc 1490 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
206 simprl 787 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
207 blcntr 22497 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
208199, 201, 206, 207syl3anc 1490 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
209 blssm 22502 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
210199, 201, 203, 209syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
211 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
212 simplll 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑)
213 rpgt0 12042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑟 ∈ ℝ+ → 0 < 𝑟)
214213ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟)
215212, 201, 203, 214, 96syl121anc 1494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
216215eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)))
217216biimpa 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
218 vex 3353 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑤 ∈ V
219218elixp 8120 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟) ↔ (𝑤 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟)))
220219simprbi 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟) → ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
221217, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
222 simp-4r 803 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘𝐼)
223 rsp 3076 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟) → (𝑘𝐼 → (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟)))
224221, 222, 223sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
225211, 224sseldd 3762 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤𝑘) ∈ 𝑢)
226210, 225ssrabdv 3841 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤𝐵 ∣ (𝑤𝑘) ∈ 𝑢})
227226, 188syl6sseqr 3812 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))
228 eleq2 2833 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝𝑦𝑝 ∈ (𝑝(ball‘𝐷)𝑟)))
229 sseq1 3786 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
230228, 229anbi12d 624 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
231230rspcev 3461 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
232205, 208, 227, 231syl12anc 865 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
233198, 232rexlimddv 3182 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
234233expr 448 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
235189, 234syl5bi 233 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
236235ralrimiv 3112 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
237157ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (MetOpen‘𝐷) ∈ Top)
238 eltop2 21059 . . . . . . . . . . . . . . . . 17 ((MetOpen‘𝐷) ∈ Top → (((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
239237, 238syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
240236, 239mpbird 248 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
241184, 240eqeltrrd 2845 . . . . . . . . . . . . . 14 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
242241ralrimiva 3113 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → ∀𝑢𝐾 ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
243159raleqdv 3292 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢𝐾 ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)))
244242, 243mpbird 248 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
245244ralrimiva 3113 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
246 fveq2 6375 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚))
247 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝑤𝑘) = (𝑤𝑚))
248247mpteq2dv 4904 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)))
249248cnveqd 5466 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚(𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)))
250249imaeq1d 5647 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))
251250eleq1d 2829 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → (((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
252246, 251raleqbidv 3300 . . . . . . . . . . . 12 (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
253252cbvralv 3319 . . . . . . . . . . 11 (∀𝑘𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
254245, 253sylib 209 . . . . . . . . . 10 (𝜑 → ∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
255 eqid 2765 . . . . . . . . . . 11 (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) = (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))
256255fmpt2x 7437 . . . . . . . . . 10 (∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
257254, 256sylib 209 . . . . . . . . 9 (𝜑 → (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
258257frnd 6230 . . . . . . . 8 (𝜑 → ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
259180, 258unssd 3951 . . . . . . 7 (𝜑 → ({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷))
260 fiss 8537 . . . . . . 7 (((MetOpen‘𝐷) ∈ Top ∧ ({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷)) → (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
261157, 259, 260syl2anc 579 . . . . . 6 (𝜑 → (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
262154, 261eqsstrd 3799 . . . . 5 (𝜑𝐶 ⊆ (fi‘(MetOpen‘𝐷)))
263 fitop 20984 . . . . . . 7 ((MetOpen‘𝐷) ∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
264157, 263syl 17 . . . . . 6 (𝜑 → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
265155mopnval 22522 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
26617, 265syl 17 . . . . . . 7 (𝜑 → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
267 tgdif0 21076 . . . . . . 7 (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran (ball‘𝐷))
268266, 267syl6eqr 2817 . . . . . 6 (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
269264, 268eqtrd 2799 . . . . 5 (𝜑 → (fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
270262, 269sseqtrd 3801 . . . 4 (𝜑𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅})))
271 2basgen 21074 . . . 4 (((ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅}))) → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
272137, 270, 271syl2anc 579 . . 3 (𝜑 → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
27311, 272eqtr4d 2802 . 2 (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
274 prdsxms.j . . 3 𝐽 = (TopOpen‘𝑌)
27513, 14, 1, 4, 274prdstopn 21711 . 2 (𝜑𝐽 = (∏t‘(TopOpen ∘ 𝑅)))
276273, 275, 2683eqtr4d 2809 1 (𝜑𝐽 = (MetOpen‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107  wal 1650   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  wss 3732  c0 4079  {csn 4334   cuni 4594   ciun 4676   class class class wbr 4809  cmpt 4888   × cxp 5275  ccnv 5276  ran crn 5278  cres 5279  cima 5280  ccom 5281   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  Xcixp 8113  Fincfn 8160  ficfi 8523  0cc0 10189  *cxr 10327   < clt 10328  +crp 12028  Basecbs 16132  distcds 16225  TopOpenctopn 16350  topGenctg 16366  tcpt 16367  Xscprds 16374  ∞Metcxmet 20004  ballcbl 20006  MetOpencmopn 20009  Topctop 20977  TopOnctopon 20994  TopSpctps 21016  ∞MetSpcxms 22401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-map 8062  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-icc 12384  df-fz 12534  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-plusg 16229  df-mulr 16230  df-sca 16232  df-vsca 16233  df-ip 16234  df-tset 16235  df-ple 16236  df-ds 16238  df-hom 16240  df-cco 16241  df-rest 16351  df-topn 16352  df-topgen 16372  df-pt 16373  df-prds 16376  df-psmet 20011  df-xmet 20012  df-bl 20014  df-mopn 20015  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-xms 22404
This theorem is referenced by:  prdsxms  22614
  Copyright terms: Public domain W3C validator