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

Theorem prdsxmslem2 23694
Description: Lemma for prdsxms 23695. 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 17145 . . . . 5 TopOpen Fn V
3 prdsxms.r . . . . . . 7 (𝜑𝑅:𝐼⟶∞MetSp)
43ffnd 6610 . . . . . 6 (𝜑𝑅 Fn 𝐼)
5 dffn2 6611 . . . . . 6 (𝑅 Fn 𝐼𝑅:𝐼⟶V)
64, 5sylib 217 . . . . 5 (𝜑𝑅:𝐼⟶V)
7 fnfco 6648 . . . . 5 ((TopOpen Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen ∘ 𝑅) Fn 𝐼)
82, 6, 7sylancr 587 . . . 4 (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼)
9 prdsxms.c . . . . 5 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))}
109ptval 22730 . . . 4 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
111, 8, 10syl2anc 584 . . 3 (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
12 eldifsn 4721 . . . . . . . 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 23693 . . . . . . . . . . 11 (𝜑𝐷 ∈ (∞Met‘𝐵))
18 blrn 23571 . . . . . . . . . . 11 (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
1917, 18syl 17 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
2017adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵))
21 simprl 768 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝑝𝐵)
22 simprr 770 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → 𝑟 ∈ ℝ*)
23 xbln0 23576 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
2420, 21, 22, 23syl3anc 1370 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
2513ad2ant1 1132 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐼 ∈ Fin)
2625mptexd 7109 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V)
27 ovex 7317 . . . . . . . . . . . . . . . . . . 19 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V
2827rgenw 3077 . . . . . . . . . . . . . . . . . 18 𝑛𝐼 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V
29 eqid 2739 . . . . . . . . . . . . . . . . . . 19 (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))
3029fnmpt 6582 . . . . . . . . . . . . . . . . . 18 (∀𝑛𝐼 ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) ∈ V → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼)
3128, 30mp1i 13 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼)
3233ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅:𝐼⟶∞MetSp)
3332ffvelrnda 6970 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → (𝑅𝑘) ∈ ∞MetSp)
34 prdsxms.v . . . . . . . . . . . . . . . . . . . . . 22 𝑉 = (Base‘(𝑅𝑘))
35 prdsxms.e . . . . . . . . . . . . . . . . . . . . . 22 𝐸 = ((dist‘(𝑅𝑘)) ↾ (𝑉 × 𝑉))
3634, 35xmsxmet 23618 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉))
3733, 36syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝐸 ∈ (∞Met‘𝑉))
38 eqid 2739 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))
39 eqid 2739 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))) = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
40143ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑆𝑊)
4133ralrimiva 3104 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 (𝑅𝑘) ∈ ∞MetSp)
42 simp2l 1198 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝𝐵)
4332feqmptd 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑘𝐼 ↦ (𝑅𝑘)))
4443oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
4513, 44eqtrid 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘))))
4645fveq2d 6787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
4716, 46eqtrid 2791 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
4842, 47eleqtrd 2842 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))))
4938, 39, 40, 25, 41, 34, 48prdsbascl 17203 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 (𝑝𝑘) ∈ 𝑉)
5049r19.21bi 3135 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → (𝑝𝑘) ∈ 𝑉)
51 simp2r 1199 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑟 ∈ ℝ*)
5251adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝑟 ∈ ℝ*)
53 eqid 2739 . . . . . . . . . . . . . . . . . . . . 21 (MetOpen‘𝐸) = (MetOpen‘𝐸)
5453blopn 23665 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝𝑘) ∈ 𝑉𝑟 ∈ ℝ*) → ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
5537, 50, 52, 54syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
56 2fveq3 6788 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → (dist‘(𝑅𝑛)) = (dist‘(𝑅𝑘)))
57 2fveq3 6788 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → (Base‘(𝑅𝑛)) = (Base‘(𝑅𝑘)))
5857, 34eqtr4di 2797 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑘 → (Base‘(𝑅𝑛)) = 𝑉)
5958sqxpeqd 5622 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛))) = (𝑉 × 𝑉))
6056, 59reseq12d 5895 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → ((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))) = ((dist‘(𝑅𝑘)) ↾ (𝑉 × 𝑉)))
6160, 35eqtr4di 2797 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → ((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))) = 𝐸)
6261fveq2d 6787 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛))))) = (ball‘𝐸))
63 fveq2 6783 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (𝑝𝑛) = (𝑝𝑘))
64 eqidd 2740 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘𝑟 = 𝑟)
6562, 63, 64oveq123d 7305 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟) = ((𝑝𝑘)(ball‘𝐸)𝑟))
66 ovex 7317 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝𝑘)(ball‘𝐸)𝑟) ∈ V
6765, 29, 66fvmpt 6884 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝐼 → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
6867adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
69 fvco3 6876 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅:𝐼⟶∞MetSp ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅𝑘)))
70 prdsxms.k . . . . . . . . . . . . . . . . . . . . . 22 𝐾 = (TopOpen‘(𝑅𝑘))
7169, 70eqtr4di 2797 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅:𝐼⟶∞MetSp ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
7232, 71sylan 580 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
7370, 34, 35xmstopn 23613 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸))
7433, 73syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → 𝐾 = (MetOpen‘𝐸))
7572, 74eqtrd 2779 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸))
7655, 68, 753eltr4d 2855 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘𝐼) → ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
7776ralrimiva 3104 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
7832feqmptd 6846 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑛𝐼 ↦ (𝑅𝑛)))
7978oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
8013, 79eqtrid 2791 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
8180fveq2d 6787 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
8215, 81eqtrid 2791 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
8382fveq2d 6787 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))))
8483oveqd 7301 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))𝑟))
85 fveq2 6783 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → (𝑅𝑛) = (𝑅𝑘))
8685cbvmptv 5188 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐼 ↦ (𝑅𝑛)) = (𝑘𝐼 ↦ (𝑅𝑘))
8786oveq2i 7295 . . . . . . . . . . . . . . . . . . 19 (𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))) = (𝑆Xs(𝑘𝐼 ↦ (𝑅𝑘)))
88 eqid 2739 . . . . . . . . . . . . . . . . . . 19 (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))) = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
89 eqid 2739 . . . . . . . . . . . . . . . . . . 19 (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))) = (dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛))))
9080fveq2d 6787 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
9116, 90eqtrid 2791 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
9242, 91eleqtrd 2842 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))
93 simp3 1137 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 0 < 𝑟)
9487, 88, 34, 35, 89, 40, 25, 33, 37, 92, 51, 93prdsbl 23656 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛𝐼 ↦ (𝑅𝑛)))))𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
9584, 94eqtrd 2779 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
96 fneq1 6533 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (𝑔 Fn 𝐼 ↔ (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼))
97 fveq1 6782 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (𝑔𝑘) = ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘))
9897eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
9998ralbidv 3113 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
10096, 99anbi12d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
10197, 67sylan9eq 2799 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∧ 𝑘𝐼) → (𝑔𝑘) = ((𝑝𝑘)(ball‘𝐸)𝑟))
102101ixpeq2dva 8709 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → X𝑘𝐼 (𝑔𝑘) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
103102eqeq2d 2750 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → ((𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)))
104100, 103anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)) ↔ (((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))))
105104spcegv 3537 . . . . . . . . . . . . . . . . . 18 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V → ((((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
1061053impib 1115 . . . . . . . . . . . . . . . . 17 (((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) ∈ V ∧ ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘𝐼 ((𝑛𝐼 ↦ ((𝑝𝑛)(ball‘((dist‘(𝑅𝑛)) ↾ ((Base‘(𝑅𝑛)) × (Base‘(𝑅𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
10726, 31, 77, 95, 106syl121anc 1374 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
1081073expia 1120 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → (0 < 𝑟 → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
10924, 108sylbid 239 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
110109adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
111 simpr 485 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → 𝑥 = (𝑝(ball‘𝐷)𝑟))
112111neeq1d 3004 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ ↔ (𝑝(ball‘𝐷)𝑟) ≠ ∅))
113 df-3an 1088 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)))
114 ral0 4444 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)
115 difeq2 4052 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝐼 → (𝐼𝑧) = (𝐼𝐼))
116 difid 4305 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼𝐼) = ∅
117115, 116eqtrdi 2795 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝐼 → (𝐼𝑧) = ∅)
118117raleqdv 3349 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)))
119118rspcev 3562 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ Fin ∧ ∀𝑘 ∈ ∅ (𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
1201, 114, 119sylancl 586 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
121120adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))
122121biantrud 532 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘))))
123113, 122bitr4id 290 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
124 eqeq1 2743 . . . . . . . . . . . . . . 15 (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘𝐼 (𝑔𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘)))
125123, 124bi2anan9 636 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
126125exbidv 1925 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 (𝑔𝑘))))
127110, 112, 1263imtr4d 294 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
128127ex 413 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝐵𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
129128rexlimdvva 3224 . . . . . . . . . 10 (𝜑 → (∃𝑝𝐵𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
13019, 129sylbid 239 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ran (ball‘𝐷) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘)))))
131130impd 411 . . . . . . . 8 (𝜑 → ((𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
13212, 131syl5bi 241 . . . . . . 7 (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
133132alrimiv 1931 . . . . . 6 (𝜑 → ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
134 ssab 3996 . . . . . 6 ((ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))} ↔ ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))))
135133, 134sylibr 233 . . . . 5 (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑔𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼𝑧)(𝑔𝑘) = ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘𝐼 (𝑔𝑘))})
136135, 9sseqtrrdi 3973 . . . 4 (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶)
137 ssv 3946 . . . . . . . . . 10 ∞MetSp ⊆ V
138 fnssres 6564 . . . . . . . . . 10 ((TopOpen Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn ∞MetSp)
1392, 137, 138mp2an 689 . . . . . . . . 9 (TopOpen ↾ ∞MetSp) Fn ∞MetSp
140 fvres 6802 . . . . . . . . . . 11 (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) = (TopOpen‘𝑥))
141 xmstps 23615 . . . . . . . . . . . 12 (𝑥 ∈ ∞MetSp → 𝑥 ∈ TopSp)
142 eqid 2739 . . . . . . . . . . . . 13 (TopOpen‘𝑥) = (TopOpen‘𝑥)
143142tpstop 22095 . . . . . . . . . . . 12 (𝑥 ∈ TopSp → (TopOpen‘𝑥) ∈ Top)
144141, 143syl 17 . . . . . . . . . . 11 (𝑥 ∈ ∞MetSp → (TopOpen‘𝑥) ∈ Top)
145140, 144eqeltrd 2840 . . . . . . . . . 10 (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top)
146145rgen 3075 . . . . . . . . 9 𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top
147 ffnfv 7001 . . . . . . . . 9 ((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ↔ ((TopOpen ↾ ∞MetSp) Fn ∞MetSp ∧ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top))
148139, 146, 147mpbir2an 708 . . . . . . . 8 (TopOpen ↾ ∞MetSp):∞MetSp⟶Top
149 fco2 6636 . . . . . . . 8 (((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen ∘ 𝑅):𝐼⟶Top)
150148, 3, 149sylancr 587 . . . . . . 7 (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top)
151 eqid 2739 . . . . . . . 8 X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)
1529, 151ptbasfi 22741 . . . . . . 7 ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅):𝐼⟶Top) → 𝐶 = (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))))
1531, 150, 152syl2anc 584 . . . . . 6 (𝜑𝐶 = (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))))
154 eqid 2739 . . . . . . . . 9 (MetOpen‘𝐷) = (MetOpen‘𝐷)
155154mopntop 23602 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top)
15617, 155syl 17 . . . . . . 7 (𝜑 → (MetOpen‘𝐷) ∈ Top)
15713, 16, 14, 1, 4prdsbas2 17189 . . . . . . . . . . . 12 (𝜑𝐵 = X𝑘𝐼 (Base‘(𝑅𝑘)))
1583, 71sylan 580 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
1593ffvelrnda 6970 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐼) → (𝑅𝑘) ∈ ∞MetSp)
160 xmstps 23615 . . . . . . . . . . . . . . . . . 18 ((𝑅𝑘) ∈ ∞MetSp → (𝑅𝑘) ∈ TopSp)
161159, 160syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐼) → (𝑅𝑘) ∈ TopSp)
16234, 70istps 22092 . . . . . . . . . . . . . . . . 17 ((𝑅𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉))
163161, 162sylib 217 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐼) → 𝐾 ∈ (TopOn‘𝑉))
164158, 163eqeltrd 2840 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉))
165 toponuni 22072 . . . . . . . . . . . . . . 15 (((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ((TopOpen ∘ 𝑅)‘𝑘))
166164, 165syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐼) → 𝑉 = ((TopOpen ∘ 𝑅)‘𝑘))
16734, 166eqtr3id 2793 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (Base‘(𝑅𝑘)) = ((TopOpen ∘ 𝑅)‘𝑘))
168167ixpeq2dva 8709 . . . . . . . . . . . 12 (𝜑X𝑘𝐼 (Base‘(𝑅𝑘)) = X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘))
169157, 168eqtrd 2779 . . . . . . . . . . 11 (𝜑𝐵 = X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘))
170 fveq2 6783 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
171170unieqd 4854 . . . . . . . . . . . 12 (𝑘 = 𝑛 ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
172171cbvixpv 8712 . . . . . . . . . . 11 X𝑘𝐼 ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)
173169, 172eqtrdi 2795 . . . . . . . . . 10 (𝜑𝐵 = X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛))
174154mopntopon 23601 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
17517, 174syl 17 . . . . . . . . . . 11 (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
176 toponmax 22084 . . . . . . . . . . 11 ((MetOpen‘𝐷) ∈ (TopOn‘𝐵) → 𝐵 ∈ (MetOpen‘𝐷))
177175, 176syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ (MetOpen‘𝐷))
178173, 177eqeltrrd 2841 . . . . . . . . 9 (𝜑X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷))
179178snssd 4743 . . . . . . . 8 (𝜑 → {X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷))
180173mpteq1d 5170 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
181180ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
182181cnveqd 5787 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)))
183182imaeq1d 5971 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢))
184 fveq1 6782 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑝 → (𝑤𝑘) = (𝑝𝑘))
185184eleq1d 2824 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑝 → ((𝑤𝑘) ∈ 𝑢 ↔ (𝑝𝑘) ∈ 𝑢))
186 eqid 2739 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝐵 ↦ (𝑤𝑘)) = (𝑤𝐵 ↦ (𝑤𝑘))
187186mptpreima 6146 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) = {𝑤𝐵 ∣ (𝑤𝑘) ∈ 𝑢}
188185, 187elrab2 3628 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))
189159, 36syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝐼) → 𝐸 ∈ (∞Met‘𝑉))
190189adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉))
191 simprl 768 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑢𝐾)
192159, 73syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘𝐼) → 𝐾 = (MetOpen‘𝐸))
193192adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸))
194191, 193eleqtrd 2842 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸))
195 simprrr 779 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → (𝑝𝑘) ∈ 𝑢)
19653mopni2 23658 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
197190, 194, 195, 196syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
19817ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵))
199 simprrl 778 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → 𝑝𝐵)
200199adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝𝐵)
201 rpxr 12748 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
202201ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*)
203154blopn 23665 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
204198, 200, 202, 203syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
205 simprl 768 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
206 blcntr 23575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
207198, 200, 205, 206syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
208 blssm 23580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝𝐵𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
209198, 200, 202, 208syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
210 simplrr 775 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
211 simplll 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑)
212 rpgt0 12751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑟 ∈ ℝ+ → 0 < 𝑟)
213212ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟)
214211, 200, 202, 213, 95syl121anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
215214eleq2d 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟)))
216215biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟))
217 vex 3437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑤 ∈ V
218217elixp 8701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟) ↔ (𝑤 Fn 𝐼 ∧ ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟)))
219218simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤X𝑘𝐼 ((𝑝𝑘)(ball‘𝐸)𝑟) → ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
220216, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
221 simp-4r 781 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘𝐼)
222 rsp 3132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑘𝐼 (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟) → (𝑘𝐼 → (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟)))
223220, 221, 222sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤𝑘) ∈ ((𝑝𝑘)(ball‘𝐸)𝑟))
224210, 223sseldd 3923 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤𝑘) ∈ 𝑢)
225209, 224ssrabdv 4008 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤𝐵 ∣ (𝑤𝑘) ∈ 𝑢})
226225, 187sseqtrrdi 3973 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))
227 eleq2 2828 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝𝑦𝑝 ∈ (𝑝(ball‘𝐷)𝑟)))
228 sseq1 3947 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
229227, 228anbi12d 631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
230229rspcev 3562 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
231204, 207, 226, 230syl12anc 834 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
232197, 231rexlimddv 3221 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘𝐼) ∧ (𝑢𝐾 ∧ (𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
233232expr 457 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑝𝐵 ∧ (𝑝𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
234188, 233syl5bi 241 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
235234ralrimiv 3103 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)))
236156ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (MetOpen‘𝐷) ∈ Top)
237 eltop2 22134 . . . . . . . . . . . . . . . . 17 ((MetOpen‘𝐷) ∈ Top → (((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
238236, 237syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → (((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝𝑦𝑦 ⊆ ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢))))
239235, 238mpbird 256 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤𝐵 ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
240183, 239eqeltrrd 2841 . . . . . . . . . . . . . 14 (((𝜑𝑘𝐼) ∧ 𝑢𝐾) → ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
241240ralrimiva 3104 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → ∀𝑢𝐾 ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
242158raleqdv 3349 . . . . . . . . . . . . 13 ((𝜑𝑘𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢𝐾 ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)))
243241, 242mpbird 256 . . . . . . . . . . . 12 ((𝜑𝑘𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
244243ralrimiva 3104 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
245 fveq2 6783 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚))
246 fveq2 6783 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝑤𝑘) = (𝑤𝑚))
247246mpteq2dv 5177 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)))
248247cnveqd 5787 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚(𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) = (𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)))
249248imaeq1d 5971 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))
250249eleq1d 2824 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → (((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
251245, 250raleqbidv 3337 . . . . . . . . . . . 12 (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
252251cbvralvw 3384 . . . . . . . . . . 11 (∀𝑘𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
253244, 252sylib 217 . . . . . . . . . 10 (𝜑 → ∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
254 eqid 2739 . . . . . . . . . . 11 (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) = (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))
255254fmpox 7916 . . . . . . . . . 10 (∀𝑚𝐼𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
256253, 255sylib 217 . . . . . . . . 9 (𝜑 → (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)): 𝑚𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
257256frnd 6617 . . . . . . . 8 (𝜑 → ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
258179, 257unssd 4121 . . . . . . 7 (𝜑 → ({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷))
259 fiss 9192 . . . . . . 7 (((MetOpen‘𝐷) ∈ Top ∧ ({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷)) → (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
260156, 258, 259syl2anc 584 . . . . . 6 (𝜑 → (fi‘({X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ ((𝑤X𝑛𝐼 ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
261153, 260eqsstrd 3960 . . . . 5 (𝜑𝐶 ⊆ (fi‘(MetOpen‘𝐷)))
262 fitop 22058 . . . . . . 7 ((MetOpen‘𝐷) ∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
263156, 262syl 17 . . . . . 6 (𝜑 → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
264154mopnval 23600 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
26517, 264syl 17 . . . . . . 7 (𝜑 → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
266 tgdif0 22151 . . . . . . 7 (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran (ball‘𝐷))
267265, 266eqtr4di 2797 . . . . . 6 (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
268263, 267eqtrd 2779 . . . . 5 (𝜑 → (fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
269261, 268sseqtrd 3962 . . . 4 (𝜑𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅})))
270 2basgen 22149 . . . 4 (((ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅}))) → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
271136, 269, 270syl2anc 584 . . 3 (𝜑 → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
27211, 271eqtr4d 2782 . 2 (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
273 prdsxms.j . . 3 𝐽 = (TopOpen‘𝑌)
27413, 14, 1, 4, 273prdstopn 22788 . 2 (𝜑𝐽 = (∏t‘(TopOpen ∘ 𝑅)))
275272, 274, 2673eqtr4d 2789 1 (𝜑𝐽 = (MetOpen‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086  wal 1537   = wceq 1539  wex 1782  wcel 2107  {cab 2716  wne 2944  wral 3065  wrex 3066  {crab 3069  Vcvv 3433  cdif 3885  cun 3886  wss 3888  c0 4257  {csn 4562   cuni 4840   ciun 4925   class class class wbr 5075  cmpt 5158   × cxp 5588  ccnv 5589  ran crn 5591  cres 5592  cima 5593  ccom 5594   Fn wfn 6432  wf 6433  cfv 6437  (class class class)co 7284  cmpo 7286  Xcixp 8694  Fincfn 8742  ficfi 9178  0cc0 10880  *cxr 11017   < clt 11018  +crp 12739  Basecbs 16921  distcds 16980  TopOpenctopn 17141  topGenctg 17157  tcpt 17158  Xscprds 17165  ∞Metcxmet 20591  ballcbl 20593  MetOpencmopn 20596  Topctop 22051  TopOnctopon 22068  TopSpctps 22090  ∞MetSpcxms 23479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-er 8507  df-map 8626  df-ixp 8695  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fi 9179  df-sup 9210  df-inf 9211  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051  df-9 12052  df-n0 12243  df-z 12329  df-dec 12447  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-icc 13095  df-fz 13249  df-struct 16857  df-slot 16892  df-ndx 16904  df-base 16922  df-plusg 16984  df-mulr 16985  df-sca 16987  df-vsca 16988  df-ip 16989  df-tset 16990  df-ple 16991  df-ds 16993  df-hom 16995  df-cco 16996  df-rest 17142  df-topn 17143  df-topgen 17163  df-pt 17164  df-prds 17167  df-psmet 20598  df-xmet 20599  df-bl 20601  df-mopn 20602  df-top 22052  df-topon 22069  df-topsp 22091  df-bases 22105  df-xms 23482
This theorem is referenced by:  prdsxms  23695
  Copyright terms: Public domain W3C validator