Theorem prdsxmslem2 23139

Description: Lemma for prdsxms 23140. 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.

Step	Hyp	Ref	Expression
1		prdsxms.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ Fin)
2		topnfn 16699	. . . . 5 ⊢ TopOpen Fn V
3		prdsxms.r	. . . . . . 7 ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp)
4	3	ffnd 6515	. . . . . 6 ⊢ (𝜑 → 𝑅 Fn 𝐼)
5		dffn2 6516	. . . . . 6 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V)
6	4, 5	sylib 220	. . . . 5 ⊢ (𝜑 → 𝑅:𝐼⟶V)
7		fnfco 6543	. . . . 5 ⊢ ((TopOpen Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen ∘ 𝑅) Fn 𝐼)
8	2, 6, 7	sylancr 589	. . . 4 ⊢ (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼)
9		prdsxms.c	. . . . 5 ⊢ 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))}
10	9	ptval 22178	. . . 4 ⊢ ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
11	1, 8, 10	syl2anc 586	. . 3 ⊢ (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
12		eldifsn 4719	. . . . . . . 8 ⊢ (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) ↔ (𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅))
13		prdsxms.y	. . . . . . . . . . . 12 ⊢ 𝑌 = (𝑆Xs𝑅)
14		prdsxms.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
15		prdsxms.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (dist‘𝑌)
16		prdsxms.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑌)
17	13, 14, 1, 15, 16, 3	prdsxmslem1 23138	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
18		blrn 23019	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
19	17, 18	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
20	17	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵))
21		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑝 ∈ 𝐵)
22		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑟 ∈ ℝ*)
23		xbln0 23024	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
24	20, 21, 22, 23	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
25	1	3ad2ant1 1129	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐼 ∈ Fin)
26	25	mptexd 6987	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V)
27		ovex 7189	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V
28	27	rgenw 3150	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑛 ∈ 𝐼 ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V
29		eqid 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))
30	29	fnmpt 6488	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ 𝐼 ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼)
31	28, 30	mp1i 13	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼)
32	3	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅:𝐼⟶∞MetSp)
33	32	ffvelrnda 6851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp)
34		prdsxms.v	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑉 = (Base‘(𝑅‘𝑘))
35		prdsxms.e	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉))
36	34, 35	xmsxmet 23066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉))
37	33, 36	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
38		eqid 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
39		eqid 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
40	14	3ad2ant1 1129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑆 ∈ 𝑊)
41	33	ralrimiva 3182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 (𝑅‘𝑘) ∈ ∞MetSp)
42		simp2l 1195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ 𝐵)
43	32	feqmptd 6733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
44	43	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
45	13, 44	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
46	45	fveq2d 6674	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
47	16, 46	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
48	42, 47	eleqtrd 2915	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
49	38, 39, 40, 25, 41, 34, 48	prdsbascl 16756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 (𝑝‘𝑘) ∈ 𝑉)
50	49	r19.21bi 3208	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑝‘𝑘) ∈ 𝑉)
51		simp2r 1196	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑟 ∈ ℝ*)
52	51	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝑟 ∈ ℝ*)
53		eqid 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (MetOpen‘𝐸) = (MetOpen‘𝐸)
54	53	blopn 23110	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝‘𝑘) ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
55	37, 50, 52, 54	syl3anc 1367	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
56		2fveq3 6675	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → (dist‘(𝑅‘𝑛)) = (dist‘(𝑅‘𝑘)))
57		2fveq3 6675	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = (Base‘(𝑅‘𝑘)))
58	57, 34	syl6eqr 2874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = 𝑉)
59	58	sqxpeqd 5587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))) = (𝑉 × 𝑉))
60	56, 59	reseq12d 5854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉)))
61	60, 35	syl6eqr 2874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = 𝐸)
62	61	fveq2d 6674	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))))) = (ball‘𝐸))
63		fveq2 6670	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (𝑝‘𝑛) = (𝑝‘𝑘))
64		eqidd 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → 𝑟 = 𝑟)
65	62, 63, 64	oveq123d 7177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
66		ovex 7189	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ V
67	65, 29, 66	fvmpt 6768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐼 → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
68	67	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
69		fvco3 6760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘)))
70		prdsxms.k	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐾 = (TopOpen‘(𝑅‘𝑘))
71	69, 70	syl6eqr 2874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
72	32, 71	sylan 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
73	70, 34, 35	xmstopn 23061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸))
74	33, 73	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸))
75	72, 74	eqtrd 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸))
76	55, 68, 75	3eltr4d 2928	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
77	76	ralrimiva 3182	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
78	32	feqmptd 6733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))
79	78	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
80	13, 79	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
81	80	fveq2d 6674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
82	15, 81	syl5eq 2868	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
83	82	fveq2d 6674	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))))
84	83	oveqd 7173	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟))
85		fveq2 6670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝑅‘𝑛) = (𝑅‘𝑘))
86	85	cbvmptv 5169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)) = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))
87	86	oveq2i 7167	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
88		eqid 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
89		eqid 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
90	80	fveq2d 6674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
91	16, 90	syl5eq 2868	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
92	42, 91	eleqtrd 2915	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
93		simp3 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 0 < 𝑟)
94	87, 88, 34, 35, 89, 40, 25, 33, 37, 92, 51, 93	prdsbl 23101	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
95	84, 94	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
96		fneq1 6444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (𝑔 Fn 𝐼 ↔ (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼))
97		fveq1 6669	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (𝑔‘𝑘) = ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘))
98	97	eleq1d 2897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
99	98	ralbidv 3197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
100	96, 99	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
101	97, 67	sylan9eq 2876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
102	101	ixpeq2dva 8476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → X𝑘 ∈ 𝐼 (𝑔‘𝑘) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
103	102	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
104	100, 103	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ (((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))))
105	104	spcegv 3597	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V → ((((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
106	105	3impib 1112	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V ∧ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
107	26, 31, 77, 95, 106	syl121anc 1371	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
108	107	3expia 1117	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (0 < 𝑟 → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
109	24, 108	sylbid 242	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
110	109	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
111		simpr 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → 𝑥 = (𝑝(ball‘𝐷)𝑟))
112	111	neeq1d 3075	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ ↔ (𝑝(ball‘𝐷)𝑟) ≠ ∅))
113		ral0 4456	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)
114		difeq2 4093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = (𝐼 ∖ 𝐼))
115		difid 4330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐼 ∖ 𝐼) = ∅
116	114, 115	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = ∅)
117	116	raleqdv 3415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)))
118	117	rspcev 3623	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
119	1, 113, 118	sylancl 588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
120	119	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
121	120	biantrud 534	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))))
122		df-3an 1085	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)))
123	121, 122	syl6rbbr 292	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
124		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
125	123, 124	bi2anan9 637	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
126	125	exbidv 1922	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
127	110, 112, 126	3imtr4d 296	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
128	127	ex 415	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
129	128	rexlimdvva 3294	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
130	19, 129	sylbid 242	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
131	130	impd 413	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
132	12, 131	syl5bi 244	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
133	132	alrimiv 1928	. . . . . 6 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
134		ssab 4041	. . . . . 6 ⊢ ((ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))} ↔ ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
135	133, 134	sylibr 236	. . . . 5 ⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))})
136	135, 9	sseqtrrdi 4018	. . . 4 ⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶)
137		ssv 3991	. . . . . . . . . 10 ⊢ ∞MetSp ⊆ V
138		fnssres 6470	. . . . . . . . . 10 ⊢ ((TopOpen Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn ∞MetSp)
139	2, 137, 138	mp2an 690	. . . . . . . . 9 ⊢ (TopOpen ↾ ∞MetSp) Fn ∞MetSp
140		fvres 6689	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) = (TopOpen‘𝑥))
141		xmstps 23063	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∞MetSp → 𝑥 ∈ TopSp)
142		eqid 2821	. . . . . . . . . . . . 13 ⊢ (TopOpen‘𝑥) = (TopOpen‘𝑥)
143	142	tpstop 21545	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ TopSp → (TopOpen‘𝑥) ∈ Top)
144	141, 143	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∞MetSp → (TopOpen‘𝑥) ∈ Top)
145	140, 144	eqeltrd 2913	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top)
146	145	rgen 3148	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top
147		ffnfv 6882	. . . . . . . . 9 ⊢ ((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ↔ ((TopOpen ↾ ∞MetSp) Fn ∞MetSp ∧ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top))
148	139, 146, 147	mpbir2an 709	. . . . . . . 8 ⊢ (TopOpen ↾ ∞MetSp):∞MetSp⟶Top
149		fco2 6533	. . . . . . . 8 ⊢ (((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen ∘ 𝑅):𝐼⟶Top)
150	148, 3, 149	sylancr 589	. . . . . . 7 ⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top)
151		eqid 2821	. . . . . . . 8 ⊢ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)
152	9, 151	ptbasfi 22189	. . . . . . 7 ⊢ ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅):𝐼⟶Top) → 𝐶 = (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))))
153	1, 150, 152	syl2anc 586	. . . . . 6 ⊢ (𝜑 → 𝐶 = (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))))
154		eqid 2821	. . . . . . . . 9 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
155	154	mopntop 23050	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top)
156	17, 155	syl 17	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘𝐷) ∈ Top)
157	13, 16, 14, 1, 4	prdsbas2 16742	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘)))
158	3, 71	sylan 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
159	3	ffvelrnda 6851	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp)
160		xmstps 23063	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → (𝑅‘𝑘) ∈ TopSp)
161	159, 160	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ TopSp)
162	34, 70	istps 21542	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅‘𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉))
163	161, 162	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 ∈ (TopOn‘𝑉))
164	158, 163	eqeltrd 2913	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉))
165		toponuni 21522	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
166	164, 165	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑉 = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
167	34, 166	syl5eqr 2870	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (Base‘(𝑅‘𝑘)) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
168	167	ixpeq2dva 8476	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘)) = X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘))
169	157, 168	eqtrd 2856	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘))
170		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
171	170	unieqd 4852	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → ∪ ((TopOpen ∘ 𝑅)‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑛))
172	171	cbvixpv 8479	. . . . . . . . . . 11 ⊢ X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)
173	169, 172	syl6eq 2872	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛))
174	154	mopntopon 23049	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
175	17, 174	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
176		toponmax 21534	. . . . . . . . . . 11 ⊢ ((MetOpen‘𝐷) ∈ (TopOn‘𝐵) → 𝐵 ∈ (MetOpen‘𝐷))
177	175, 176	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (MetOpen‘𝐷))
178	173, 177	eqeltrrd 2914	. . . . . . . . 9 ⊢ (𝜑 → X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷))
179	178	snssd 4742	. . . . . . . 8 ⊢ (𝜑 → {X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷))
180	173	mpteq1d 5155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
181	180	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
182	181	cnveqd 5746	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
183	182	imaeq1d 5928	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))
184		fveq1 6669	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑝 → (𝑤‘𝑘) = (𝑝‘𝑘))
185	184	eleq1d 2897	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑝 → ((𝑤‘𝑘) ∈ 𝑢 ↔ (𝑝‘𝑘) ∈ 𝑢))
186		eqid 2821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘))
187	186	mptpreima 6092	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢}
188	185, 187	elrab2 3683	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))
189	159, 36	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
190	189	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉))
191		simprl 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ 𝐾)
192	159, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸))
193	192	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸))
194	191, 193	eleqtrd 2915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸))
195		simprrr 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → (𝑝‘𝑘) ∈ 𝑢)
196	53	mopni2 23103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
197	190, 194, 195, 196	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
198	17	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵))
199		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑝 ∈ 𝐵)
200	199	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ 𝐵)
201		rpxr 12399	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
202	201	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*)
203	154	blopn 23110	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
204	198, 200, 202, 203	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
205		simprl 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
206		blcntr 23023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
207	198, 200, 205, 206	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
208		blssm 23028	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
209	198, 200, 202, 208	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
210		simplrr 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
211		simplll 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑)
212		rpgt0 12402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑟 ∈ ℝ+ → 0 < 𝑟)
213	212	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟)
214	211, 200, 202, 213, 95	syl121anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
215	214	eleq2d 2898	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
216	215	biimpa 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
217		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑤 ∈ V
218	217	elixp 8468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟) ↔ (𝑤 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
219	218	simprbi 499	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟) → ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
220	216, 219	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
221		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘 ∈ 𝐼)
222		rsp 3205	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟) → (𝑘 ∈ 𝐼 → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
223	220, 221, 222	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
224	210, 223	sseldd 3968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ 𝑢)
225	209, 224	ssrabdv 4050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢})
226	225, 187	sseqtrrdi 4018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))
227		eleq2 2901	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝 ∈ 𝑦 ↔ 𝑝 ∈ (𝑝(ball‘𝐷)𝑟)))
228		sseq1 3992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
229	227, 228	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
230	229	rspcev 3623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
231	204, 207, 226, 230	syl12anc 834	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
232	197, 231	rexlimddv 3291	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
233	232	expr 459	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
234	188, 233	syl5bi 244	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
235	234	ralrimiv 3181	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
236	156	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (MetOpen‘𝐷) ∈ Top)
237		eltop2 21583	. . . . . . . . . . . . . . . . 17 ⊢ ((MetOpen‘𝐷) ∈ Top → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
238	236, 237	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
239	235, 238	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
240	183, 239	eqeltrrd 2914	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
241	240	ralrimiva 3182	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
242	158	raleqdv 3415	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)))
243	241, 242	mpbird 259	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
244	243	ralrimiva 3182	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
245		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚))
246		fveq2 6670	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑚 → (𝑤‘𝑘) = (𝑤‘𝑚))
247	246	mpteq2dv 5162	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑚 → (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)))
248	247	cnveqd 5746	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑚 → ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)))
249	248	imaeq1d 5928	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑚 → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))
250	249	eleq1d 2897	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → ((◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
251	245, 250	raleqbidv 3401	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
252	251	cbvralvw 3449	. . . . . . . . . . 11 ⊢ (∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
253	244, 252	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
254		eqid 2821	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) = (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))
255	254	fmpox 7765	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
256	253, 255	sylib 220	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
257	256	frnd 6521	. . . . . . . 8 ⊢ (𝜑 → ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
258	179, 257	unssd 4162	. . . . . . 7 ⊢ (𝜑 → ({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷))
259		fiss 8888	. . . . . . 7 ⊢ (((MetOpen‘𝐷) ∈ Top ∧ ({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷)) → (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
260	156, 258, 259	syl2anc 586	. . . . . 6 ⊢ (𝜑 → (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
261	153, 260	eqsstrd 4005	. . . . 5 ⊢ (𝜑 → 𝐶 ⊆ (fi‘(MetOpen‘𝐷)))
262		fitop 21508	. . . . . . 7 ⊢ ((MetOpen‘𝐷) ∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
263	156, 262	syl 17	. . . . . 6 ⊢ (𝜑 → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
264	154	mopnval 23048	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
265	17, 264	syl 17	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
266		tgdif0 21600	. . . . . . 7 ⊢ (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran (ball‘𝐷))
267	265, 266	syl6eqr 2874	. . . . . 6 ⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
268	263, 267	eqtrd 2856	. . . . 5 ⊢ (𝜑 → (fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
269	261, 268	sseqtrd 4007	. . . 4 ⊢ (𝜑 → 𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅})))
270		2basgen 21598	. . . 4 ⊢ (((ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅}))) → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
271	136, 269, 270	syl2anc 586	. . 3 ⊢ (𝜑 → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
272	11, 271	eqtr4d 2859	. 2 ⊢ (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
273		prdsxms.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝑌)
274	13, 14, 1, 4, 273	prdstopn 22236	. 2 ⊢ (𝜑 → 𝐽 = (∏t‘(TopOpen ∘ 𝑅)))
275	272, 274, 267	3eqtr4d 2866	1 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2799   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3494   ∖ cdif 3933   ∪ cun 3934   ⊆ wss 3936  ∅c0 4291  {csn 4567  ∪ cuni 4838  ∪ ciun 4919   class class class wbr 5066   ↦ cmpt 5146   × cxp 5553  ^◡ccnv 5554  ran crn 5556   ↾ cres 5557   “ cima 5558   ∘ ccom 5559   Fn wfn 6350  ⟶wf 6351  ‘cfv 6355  (class class class)co 7156   ∈ cmpo 7158  Xcixp 8461  Fincfn 8509  ficfi 8874  0cc0 10537  ℝ^*cxr 10674   < clt 10675  ℝ⁺crp 12390  Basecbs 16483  distcds 16574  TopOpenctopn 16695  topGenctg 16711  ∏_tcpt 16712  X_scprds 16719  ∞Metcxmet 20530  ballcbl 20532  MetOpencmopn 20535  Topctop 21501  TopOnctopon 21518  TopSpctps 21540  ∞MetSpcxms 22927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-iin 4922  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-oadd 8106  df-er 8289  df-map 8408  df-ixp 8462  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-fi 8875  df-sup 8906  df-inf 8907  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11639  df-2 11701  df-3 11702  df-4 11703  df-5 11704  df-6 11705  df-7 11706  df-8 11707  df-9 11708  df-n0 11899  df-z 11983  df-dec 12100  df-uz 12245  df-q 12350  df-rp 12391  df-xneg 12508  df-xadd 12509  df-xmul 12510  df-icc 12746  df-fz 12894  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-plusg 16578  df-mulr 16579  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-hom 16589  df-cco 16590  df-rest 16696  df-topn 16697  df-topgen 16717  df-pt 16718  df-prds 16721  df-psmet 20537  df-xmet 20538  df-bl 20540  df-mopn 20541  df-top 21502  df-topon 21519  df-topsp 21541  df-bases 21554  df-xms 22930

This theorem is referenced by:  prdsxms  23140