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

Theorem prdsxmslem2 22704
 Description: Lemma for prdsxms 22705. 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 16439 . . . . 5 TopOpen Fn V
3 prdsxms.r . . . . . . 7 (𝜑𝑅:𝐼⟶∞MetSp)
43ffnd 6279 . . . . . 6 (𝜑𝑅 Fn 𝐼)
5 dffn2 6280 . . . . . 6 (𝑅 Fn 𝐼𝑅:𝐼⟶V)
64, 5sylib 210 . . . . 5 (𝜑𝑅:𝐼⟶V)
7 fnfco 6306 . . . . 5 ((TopOpen Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen ∘ 𝑅) Fn 𝐼)
82, 6, 7sylancr 581 . . . 4 (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼)
9 prdsxms.c . . . . 5 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))}
109ptval 21744 . . . 4 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
111, 8, 10syl2anc 579 . . 3 (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
12 eldifsn 4536 . . . . . . . 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 22703 . . . . . . . . . . 11 (𝜑𝐷 ∈ (∞Met‘𝐵))
18 blrn 22584 . . . . . . . . . . 11 (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
1917, 18syl 17 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
2017adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵))
21 simprl 787 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝑝𝐵)
22 simprr 789 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝑟 ∈ ℝ*)
23 xbln0 22589 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
2420, 21, 22, 23syl3anc 1494 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
2513ad2ant1 1167 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐼 ∈ Fin)
26 mptexg 6740 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ Fin → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V)
2725, 26syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V)
28 ovex 6937 . . . . . . . . . . . . . . . . . . 19 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V
2928rgenw 3133 . . . . . . . . . . . . . . . . . 18 𝑛𝐼 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V
30 eqid 2825 . . . . . . . . . . . . . . . . . . 19 (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))
3130fnmpt 6253 . . . . . . . . . . . . . . . . . 18 (∀𝑛𝐼 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼)
3229, 31mp1i 13 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼)
3333ad2ant1 1167 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅:𝐼⟶∞MetSp)
3433ffvelrnda 6608 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → (𝑅𝑘) ∈ ∞MetSp)
35 prdsxms.v . . . . . . . . . . . . . . . . . . . . . 22 𝑉 = (Base‘(𝑅𝑘))
36 prdsxms.e . . . . . . . . . . . . . . . . . . . . . 22 𝐸 = ((dist‘(𝑅𝑘)) ↾ (𝑉 × 𝑉))
3735, 36xmsxmet 22631 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉))
3834, 37syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝐸 ∈ (∞Met‘𝑉))
39 eqid 2825 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))
40 eqid 2825 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))) = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
41143ad2ant1 1167 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑆𝑊)
4234ralrimiva 3175 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 (𝑅𝑘) ∈ ∞MetSp)
43 simp2l 1260 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝𝐵)
4433feqmptd 6496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑘𝐼 ↦ (𝑅𝑘)))
4544oveq2d 6921 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
4613, 45syl5eq 2873 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
4746fveq2d 6437 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
4816, 47syl5eq 2873 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
4943, 48eleqtrd 2908 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
5039, 40, 41, 25, 42, 35, 49prdsbascl 16496 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 (𝑝𝑘) ∈ 𝑉)
5150r19.21bi 3141 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → (𝑝𝑘) ∈ 𝑉)
52 simp2r 1261 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑟 ∈ ℝ*)
5352adantr 474 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝑟 ∈ ℝ*)
54 eqid 2825 . . . . . . . . . . . . . . . . . . . . 21 (MetOpen‘𝐸) = (MetOpen‘𝐸)
5554blopn 22675 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝𝑘) ∈ 𝑉𝑟 ∈ ℝ*) → ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
5638, 51, 53, 55syl3anc 1494 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
57 2fveq3 6438 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → (dist‘(𝑅𝑛)) = (dist‘(𝑅𝑘)))
58 2fveq3 6438 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → (Base‘(𝑅𝑛)) = (Base‘(𝑅𝑘)))
5958, 35syl6eqr 2879 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑘 → (Base‘(𝑅𝑛)) = 𝑉)
6059sqxpeqd 5374 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛))) = (𝑉 × 𝑉))
6157, 60reseq12d 5630 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → ((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))) = ((dist‘(𝑅𝑘)) ↾ (𝑉 × 𝑉)))
6261, 36syl6eqr 2879 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → ((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))) = 𝐸)
6362fveq2d 6437 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛))))) = (ball‘𝐸))
64 fveq2 6433 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (𝑝𝑛) = (𝑝𝑘))
65 eqidd 2826 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘𝑟 = 𝑟)
6663, 64, 65oveq123d 6926 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) = ((𝑝𝑘)(ball‘𝐸)𝑟))
67 ovex 6937 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ V
6866, 30, 67fvmpt 6529 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝐼 → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
6968adantl 475 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
70 fvco3 6522 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅:𝐼⟶∞MetSp ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅𝑘)))
71 prdsxms.k . . . . . . . . . . . . . . . . . . . . . 22 𝐾 = (TopOpen‘(𝑅𝑘))
7270, 71syl6eqr 2879 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅:𝐼⟶∞MetSp ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
7333, 72sylan 575 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
7471, 35, 36xmstopn 22626 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸))
7534, 74syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝐾 = (MetOpen‘𝐸))
7673, 75eqtrd 2861 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸))
7756, 69, 763eltr4d 2921 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
7877ralrimiva 3175 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
7933feqmptd 6496 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑛𝐼 ↦ (𝑅𝑛)))
8079oveq2d 6921 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
8113, 80syl5eq 2873 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
8281fveq2d 6437 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
8315, 82syl5eq 2873 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
8483fveq2d 6437 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))))
8584oveqd 6922 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))𝑟))
86 fveq2 6433 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → (𝑅𝑛) = (𝑅𝑘))
8786cbvmptv 4973 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐼 ↦ (𝑅𝑛)) = (𝑘𝐼 ↦ (𝑅𝑘))
8887oveq2i 6916 . . . . . . . . . . . . . . . . . . 19 (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))
89 eqid 2825 . . . . . . . . . . . . . . . . . . 19 (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))) = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
90 eqid 2825 . . . . . . . . . . . . . . . . . . 19 (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))) = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
9181fveq2d 6437 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
9216, 91syl5eq 2873 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
9343, 92eleqtrd 2908 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
94 simp3 1172 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 0 < 𝑟)
9588, 89, 35, 36, 90, 41, 25, 34, 38, 93, 52, 94prdsbl 22666 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
9685, 95eqtrd 2861 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
97 fneq1 6212 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (𝑔 Fn 𝐼 ↔ (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼))
98 fveq1 6432 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (𝑔𝑘) = ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘))
9998eleq1d 2891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
10099ralbidv 3195 . . . . . . . . . . . . . . . . . . . . 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 2881 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∧ 𝑘𝐼) → (𝑔𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
103102ixpeq2dva 8190 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → X𝑘𝐼 (𝑔𝑘) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
104103eqeq2d 2835 . . . . . . . . . . . . . . . . . . . 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 3511 . . . . . . . . . . . . . . . . . 18 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V → ((((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
1071063impib 1148 . . . . . . . . . . . . . . . . 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 1498 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
1091083expia 1154 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → (0 < 𝑟 → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
11024, 109sylbid 232 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
111110adantr 474 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
112 simpr 479 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → 𝑥 = (𝑝(ball‘𝐷)𝑟))
113112neeq1d 3058 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ ↔ (𝑝(ball‘𝐷)𝑟) ≠ ∅))
114 ral0 4298 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)
115 difeq2 3949 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝐼 → (𝐼𝑧) = (𝐼𝐼))
116 difid 4178 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝐼) = ∅
117115, 116syl6eq 2877 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝐼 → (𝐼𝑧) = ∅)
118117raleqdv 3356 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)))
119118rspcev 3526 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ Fin ∧ ∀𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
1201, 114, 119sylancl 580 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
121120adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
122121biantrud 527 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))))
123 df-3an 1113 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)))
124122, 123syl6rbbr 282 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
125 eqeq1 2829 . . . . . . . . . . . . . . 15 (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘𝐼 (𝑔𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
126124, 125bi2anan9 629 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
127126exbidv 2020 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
128111, 113, 1273imtr4d 286 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
129128ex 403 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
130129rexlimdvva 3248 . . . . . . . . . 10 (𝜑 → (∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
13119, 130sylbid 232 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ran (ball‘𝐷) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
132131impd 400 . . . . . . . 8 (𝜑 → ((𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
13312, 132syl5bi 234 . . . . . . 7 (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
134133alrimiv 2026 . . . . . 6 (𝜑 → ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
135 ssab 3897 . . . . . 6 ((ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))} ↔ ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
136134, 135sylibr 226 . . . . 5 (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))})
137136, 9syl6sseqr 3877 . . . 4 (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶)
138 ssv 3850 . . . . . . . . . 10 ∞MetSp ⊆ V
139 fnssres 6237 . . . . . . . . . 10 ((TopOpen Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn ∞MetSp)
1402, 138, 139mp2an 683 . . . . . . . . 9 (TopOpen ↾ ∞MetSp) Fn ∞MetSp
141 fvres 6452 . . . . . . . . . . 11 (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) = (TopOpen‘𝑥))
142 xmstps 22628 . . . . . . . . . . . 12 (𝑥 ∈ ∞MetSp → 𝑥 ∈ TopSp)
143 eqid 2825 . . . . . . . . . . . . 13 (TopOpen‘𝑥) = (TopOpen‘𝑥)
144143tpstop 21112 . . . . . . . . . . . 12 (𝑥 ∈ TopSp → (TopOpen‘𝑥) ∈ Top)
145142, 144syl 17 . . . . . . . . . . 11 (𝑥 ∈ ∞MetSp → (TopOpen‘𝑥) ∈ Top)
146141, 145eqeltrd 2906 . . . . . . . . . 10 (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top)
147146rgen 3131 . . . . . . . . 9 𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top
148 ffnfv 6637 . . . . . . . . 9 ((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ↔ ((TopOpen ↾ ∞MetSp) Fn ∞MetSp ∧ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top))
149140, 147, 148mpbir2an 702 . . . . . . . 8 (TopOpen ↾ ∞MetSp):∞MetSp⟶Top
150 fco2 6296 . . . . . . . 8 (((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen ∘ 𝑅):𝐼⟶Top)
151149, 3, 150sylancr 581 . . . . . . 7 (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top)
152 eqid 2825 . . . . . . . 8 X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)
1539, 152ptbasfi 21755 . . . . . . 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 2825 . . . . . . . . 9 (MetOpen‘𝐷) = (MetOpen‘𝐷)
156155mopntop 22615 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top)
15717, 156syl 17 . . . . . . 7 (𝜑 → (MetOpen‘𝐷) ∈ Top)
15813, 16, 14, 1, 4prdsbas2 16482 . . . . . . . . . . . 12 (𝜑𝐵 = X𝑘𝐼 (Base‘(𝑅𝑘)))
1593, 72sylan 575 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
1603ffvelrnda 6608 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → (𝑅𝑘) ∈ ∞MetSp)
161 xmstps 22628 . . . . . . . . . . . . . . . . . 18 ((𝑅𝑘) ∈ ∞MetSp → (𝑅𝑘) ∈ TopSp)
162160, 161syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑅𝑘) ∈ TopSp)
16335, 71istps 21109 . . . . . . . . . . . . . . . . 17 ((𝑅𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉))
164162, 163sylib 210 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → 𝐾 ∈ (TopOn‘𝑉))
165159, 164eqeltrd 2906 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉))
166 toponuni 21089 . . . . . . . . . . . . . . 15 (((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ((TopOpen ∘ 𝑅)‘𝑘))
167165, 166syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐼) → 𝑉 = ((TopOpen ∘ 𝑅)‘𝑘))
16835, 167syl5eqr 2875 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (Base‘(𝑅𝑘)) = ((TopOpen ∘ 𝑅)‘𝑘))
169168ixpeq2dva 8190 . . . . . . . . . . . 12 (𝜑X𝑘𝐼 (Base‘(𝑅𝑘)) = X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘))
170158, 169eqtrd 2861 . . . . . . . . . . 11 (𝜑𝐵 = X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘))
171 fveq2 6433 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
172171unieqd 4668 . . . . . . . . . . . 12 (𝑘 = 𝑛 ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
173172cbvixpv 8193 . . . . . . . . . . 11 X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)
174170, 173syl6eq 2877 . . . . . . . . . 10 (𝜑𝐵 = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛))
175155mopntopon 22614 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
17617, 175syl 17 . . . . . . . . . . 11 (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
177 toponmax 21101 . . . . . . . . . . 11 ((MetOpen‘𝐷) ∈ (TopOn‘𝐵) → 𝐵 ∈ (MetOpen‘𝐷))
178176, 177syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ (MetOpen‘𝐷))
179174, 178eqeltrrd 2907 . . . . . . . . 9 (𝜑X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷))
180179snssd 4558 . . . . . . . 8 (𝜑 → {X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷))
181174mpteq1d 4961 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
182181ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
183182cnveqd 5530 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
184183imaeq1d 5706 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢))
185 fveq1 6432 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑝 → (𝑤𝑘) = (𝑝𝑘))
186185eleq1d 2891 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑝 → ((𝑤𝑘) ∈ 𝑢 ↔ (𝑝𝑘) ∈ 𝑢))
187 eqid 2825 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤𝐵 ↦ (𝑤𝑘))
188187mptpreima 5869 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) = {𝑤𝐵 ∣ (𝑤𝑘) ∈ 𝑢}
189186, 188elrab2 3589 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))
190160, 37syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝐼) → 𝐸 ∈ (∞Met‘𝑉))
191190adantr 474 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉))
192 simprl 787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑢𝐾)
193160, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝐼) → 𝐾 = (MetOpen‘𝐸))
194193adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸))
195192, 194eleqtrd 2908 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸))
196 simprrr 800 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → (𝑝𝑘) ∈ 𝑢)
19754mopni2 22668 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
198191, 195, 196, 197syl3anc 1494 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
19917ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵))
200 simprrl 799 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑝𝐵)
201200adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝𝐵)
202 rpxr 12123 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
203202ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*)
204155blopn 22675 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
205199, 201, 203, 204syl3anc 1494 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
206 simprl 787 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
207 blcntr 22588 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
208199, 201, 206, 207syl3anc 1494 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
209 blssm 22593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
210199, 201, 203, 209syl3anc 1494 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
211 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
212 simplll 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑)
213 rpgt0 12126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑟 ∈ ℝ+ → 0 < 𝑟)
214213ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟)
215212, 201, 203, 214, 96syl121anc 1498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
216215eleq2d 2892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)))
217216biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
218 vex 3417 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑤 ∈ V
219218elixp 8182 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟) ↔ (𝑤 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟)))
220219simprbi 492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟) → ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
221217, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
222 simp-4r 803 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘𝐼)
223 rsp 3138 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟) → (𝑘𝐼 → (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟)))
224221, 222, 223sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
225211, 224sseldd 3828 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤𝑘) ∈ 𝑢)
226210, 225ssrabdv 3906 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤𝐵 ∣ (𝑤𝑘) ∈ 𝑢})
227226, 188syl6sseqr 3877 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))
228 eleq2 2895 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝𝑦𝑝 ∈ (𝑝(ball‘𝐷)𝑟)))
229 sseq1 3851 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
230228, 229anbi12d 624 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
231230rspcev 3526 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
232205, 208, 227, 231syl12anc 870 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
233198, 232rexlimddv 3245 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
234233expr 450 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
235189, 234syl5bi 234 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
236235ralrimiv 3174 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
237157ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (MetOpen‘𝐷) ∈ Top)
238 eltop2 21150 . . . . . . . . . . . . . . . . 17 ((MetOpen‘𝐷) ∈ Top → (((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
239237, 238syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
240236, 239mpbird 249 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
241184, 240eqeltrrd 2907 . . . . . . . . . . . . . 14 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
242241ralrimiva 3175 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → ∀𝑢𝐾 ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
243159raleqdv 3356 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢𝐾 ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)))
244242, 243mpbird 249 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
245244ralrimiva 3175 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
246 fveq2 6433 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚))
247 fveq2 6433 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝑤𝑘) = (𝑤𝑚))
248247mpteq2dv 4968 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)))
249248cnveqd 5530 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚(𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)))
250249imaeq1d 5706 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))
251250eleq1d 2891 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → (((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
252246, 251raleqbidv 3364 . . . . . . . . . . . 12 (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
253252cbvralv 3383 . . . . . . . . . . 11 (∀𝑘𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
254245, 253sylib 210 . . . . . . . . . 10 (𝜑 → ∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
255 eqid 2825 . . . . . . . . . . 11 (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) = (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))
256255fmpt2x 7499 . . . . . . . . . 10 (∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
257254, 256sylib 210 . . . . . . . . 9 (𝜑 → (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
258257frnd 6285 . . . . . . . 8 (𝜑 → ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
259180, 258unssd 4016 . . . . . . 7 (𝜑 → ({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷))
260 fiss 8599 . . . . . . 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 3864 . . . . 5 (𝜑𝐶 ⊆ (fi‘(MetOpen‘𝐷)))
263 fitop 21075 . . . . . . 7 ((MetOpen‘𝐷) ∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
264157, 263syl 17 . . . . . 6 (𝜑 → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
265155mopnval 22613 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
26617, 265syl 17 . . . . . . 7 (𝜑 → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
267 tgdif0 21167 . . . . . . 7 (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran (ball‘𝐷))
268266, 267syl6eqr 2879 . . . . . 6 (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
269264, 268eqtrd 2861 . . . . 5 (𝜑 → (fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
270262, 269sseqtrd 3866 . . . 4 (𝜑𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅})))
271 2basgen 21165 . . . 4 (((ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅}))) → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
272137, 270, 271syl2anc 579 . . 3 (𝜑 → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
27311, 272eqtr4d 2864 . 2 (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
274 prdsxms.j . . 3 𝐽 = (TopOpen‘𝑌)
27513, 14, 1, 4, 274prdstopn 21802 . 2 (𝜑𝐽 = (∏t‘(TopOpen ∘ 𝑅)))
276273, 275, 2683eqtr4d 2871 1 (𝜑𝐽 = (MetOpen‘𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1111  ∀wal 1654   = wceq 1656  ∃wex 1878   ∈ wcel 2164  {cab 2811   ≠ wne 2999  ∀wral 3117  ∃wrex 3118  {crab 3121  Vcvv 3414   ∖ cdif 3795   ∪ cun 3796   ⊆ wss 3798  ∅c0 4144  {csn 4397  ∪ cuni 4658  ∪ ciun 4740   class class class wbr 4873   ↦ cmpt 4952   × cxp 5340  ◡ccnv 5341  ran crn 5343   ↾ cres 5344   “ cima 5345   ∘ ccom 5346   Fn wfn 6118  ⟶wf 6119  ‘cfv 6123  (class class class)co 6905   ↦ cmpt2 6907  Xcixp 8175  Fincfn 8222  ficfi 8585  0cc0 10252  ℝ*cxr 10390   < clt 10391  ℝ+crp 12112  Basecbs 16222  distcds 16314  TopOpenctopn 16435  topGenctg 16451  ∏tcpt 16452  Xscprds 16459  ∞Metcxmet 20091  ballcbl 20093  MetOpencmopn 20096  Topctop 21068  TopOnctopon 21085  TopSpctps 21107  ∞MetSpcxms 22492 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-iin 4743  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-oadd 7830  df-er 8009  df-map 8124  df-ixp 8176  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-fi 8586  df-sup 8617  df-inf 8618  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420  df-9 11421  df-n0 11619  df-z 11705  df-dec 11822  df-uz 11969  df-q 12072  df-rp 12113  df-xneg 12232  df-xadd 12233  df-xmul 12234  df-icc 12470  df-fz 12620  df-struct 16224  df-ndx 16225  df-slot 16226  df-base 16228  df-plusg 16318  df-mulr 16319  df-sca 16321  df-vsca 16322  df-ip 16323  df-tset 16324  df-ple 16325  df-ds 16327  df-hom 16329  df-cco 16330  df-rest 16436  df-topn 16437  df-topgen 16457  df-pt 16458  df-prds 16461  df-psmet 20098  df-xmet 20099  df-bl 20101  df-mopn 20102  df-top 21069  df-topon 21086  df-topsp 21108  df-bases 21121  df-xms 22495 This theorem is referenced by:  prdsxms  22705
 Copyright terms: Public domain W3C validator