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.

Step	Hyp	Ref	Expression
1		prdsxms.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ Fin)
2		topnfn 16439	. . . . 5 ⊢ TopOpen Fn V
3		prdsxms.r	. . . . . . 7 ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp)
4	3	ffnd 6279	. . . . . 6 ⊢ (𝜑 → 𝑅 Fn 𝐼)
5		dffn2 6280	. . . . . 6 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V)
6	4, 5	sylib 210	. . . . 5 ⊢ (𝜑 → 𝑅:𝐼⟶V)
7		fnfco 6306	. . . . 5 ⊢ ((TopOpen Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen ∘ 𝑅) Fn 𝐼)
8	2, 6, 7	sylancr 581	. . . 4 ⊢ (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼)
9		prdsxms.c	. . . . 5 ⊢ 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))}
10	9	ptval 21744	. . . 4 ⊢ ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
11	1, 8, 10	syl2anc 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‘𝑌)
17	13, 14, 1, 15, 16, 3	prdsxmslem1 22703	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
18		blrn 22584	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
19	17, 18	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
20	17	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵))
21		simprl 787	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑝 ∈ 𝐵)
22		simprr 789	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑟 ∈ ℝ*)
23		xbln0 22589	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
24	20, 21, 22, 23	syl3anc 1494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
25	1	3ad2ant1 1167	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐼 ∈ Fin)
26		mptexg 6740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ Fin → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V)
27	25, 26	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V)
28		ovex 6937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V
29	28	rgenw 3133	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑛 ∈ 𝐼 ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V
30		eqid 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))
31	30	fnmpt 6253	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ 𝐼 ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼)
32	29, 31	mp1i 13	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼)
33	3	3ad2ant1 1167	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅:𝐼⟶∞MetSp)
34	33	ffvelrnda 6608	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp)
35		prdsxms.v	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑉 = (Base‘(𝑅‘𝑘))
36		prdsxms.e	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉))
37	35, 36	xmsxmet 22631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉))
38	34, 37	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
39		eqid 2825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
40		eqid 2825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
41	14	3ad2ant1 1167	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑆 ∈ 𝑊)
42	34	ralrimiva 3175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 (𝑅‘𝑘) ∈ ∞MetSp)
43		simp2l 1260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ 𝐵)
44	33	feqmptd 6496	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
45	44	oveq2d 6921	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
46	13, 45	syl5eq 2873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
47	46	fveq2d 6437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
48	16, 47	syl5eq 2873	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
49	43, 48	eleqtrd 2908	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
50	39, 40, 41, 25, 42, 35, 49	prdsbascl 16496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 (𝑝‘𝑘) ∈ 𝑉)
51	50	r19.21bi 3141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑝‘𝑘) ∈ 𝑉)
52		simp2r 1261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑟 ∈ ℝ*)
53	52	adantr 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝑟 ∈ ℝ*)
54		eqid 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (MetOpen‘𝐸) = (MetOpen‘𝐸)
55	54	blopn 22675	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝‘𝑘) ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
56	38, 51, 53, 55	syl3anc 1494	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
57		2fveq3 6438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → (dist‘(𝑅‘𝑛)) = (dist‘(𝑅‘𝑘)))
58		2fveq3 6438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = (Base‘(𝑅‘𝑘)))
59	58, 35	syl6eqr 2879	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = 𝑉)
60	59	sqxpeqd 5374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))) = (𝑉 × 𝑉))
61	57, 60	reseq12d 5630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉)))
62	61, 36	syl6eqr 2879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = 𝐸)
63	62	fveq2d 6437	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))))) = (ball‘𝐸))
64		fveq2 6433	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (𝑝‘𝑛) = (𝑝‘𝑘))
65		eqidd 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → 𝑟 = 𝑟)
66	63, 64, 65	oveq123d 6926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
67		ovex 6937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ V
68	66, 30, 67	fvmpt 6529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐼 → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
69	68	adantl 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
70		fvco3 6522	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘)))
71		prdsxms.k	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐾 = (TopOpen‘(𝑅‘𝑘))
72	70, 71	syl6eqr 2879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
73	33, 72	sylan 575	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
74	71, 35, 36	xmstopn 22626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸))
75	34, 74	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸))
76	73, 75	eqtrd 2861	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸))
77	56, 69, 76	3eltr4d 2921	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
78	77	ralrimiva 3175	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
79	33	feqmptd 6496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))
80	79	oveq2d 6921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
81	13, 80	syl5eq 2873	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
82	81	fveq2d 6437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
83	15, 82	syl5eq 2873	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
84	83	fveq2d 6437	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))))
85	84	oveqd 6922	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟))
86		fveq2 6433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝑅‘𝑛) = (𝑅‘𝑘))
87	86	cbvmptv 4973	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)) = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))
88	87	oveq2i 6916	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
89		eqid 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
90		eqid 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
91	81	fveq2d 6437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
92	16, 91	syl5eq 2873	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
93	43, 92	eleqtrd 2908	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
94		simp3 1172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 0 < 𝑟)
95	88, 89, 35, 36, 90, 41, 25, 34, 38, 93, 52, 94	prdsbl 22666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
96	85, 95	eqtrd 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‘(𝑅‘𝑛)))))𝑟))‘𝑘))
99	98	eleq1d 2891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
100	99	ralbidv 3195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
101	97, 100	anbi12d 624	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
102	98, 68	sylan9eq 2881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
103	102	ixpeq2dva 8190	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → X𝑘 ∈ 𝐼 (𝑔‘𝑘) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
104	103	eqeq2d 2835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
105	101, 104	anbi12d 624	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ (((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))))
106	105	spcegv 3511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V → ((((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
107	106	3impib 1148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V ∧ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
108	27, 32, 78, 96, 107	syl121anc 1498	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
109	108	3expia 1154	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (0 < 𝑟 → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
110	24, 109	sylbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
111	110	adantr 474	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
112		simpr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → 𝑥 = (𝑝(ball‘𝐷)𝑟))
113	112	neeq1d 3058	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ ↔ (𝑝(ball‘𝐷)𝑟) ≠ ∅))
114		ral0 4298	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)
115		difeq2 3949	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = (𝐼 ∖ 𝐼))
116		difid 4178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐼 ∖ 𝐼) = ∅
117	115, 116	syl6eq 2877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = ∅)
118	117	raleqdv 3356	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)))
119	118	rspcev 3526	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
120	1, 114, 119	sylancl 580	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
121	120	adantr 474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
122	121	biantrud 527	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))))
123		df-3an 1113	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)))
124	122, 123	syl6rbbr 282	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
125		eqeq1 2829	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
126	124, 125	bi2anan9 629	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
127	126	exbidv 2020	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
128	111, 113, 127	3imtr4d 286	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
129	128	ex 403	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
130	129	rexlimdvva 3248	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
131	19, 130	sylbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
132	131	impd 400	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
133	12, 132	syl5bi 234	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
134	133	alrimiv 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𝑘 ∈ 𝐼 (𝑔‘𝑘))))
136	134, 135	sylibr 226	. . . . 5 ⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))})
137	136, 9	syl6sseqr 3877	. . . 4 ⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶)
138		ssv 3850	. . . . . . . . . 10 ⊢ ∞MetSp ⊆ V
139		fnssres 6237	. . . . . . . . . 10 ⊢ ((TopOpen Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn ∞MetSp)
140	2, 138, 139	mp2an 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‘𝑥)
144	143	tpstop 21112	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ TopSp → (TopOpen‘𝑥) ∈ Top)
145	142, 144	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∞MetSp → (TopOpen‘𝑥) ∈ Top)
146	141, 145	eqeltrd 2906	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top)
147	146	rgen 3131	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top
148		ffnfv 6637	. . . . . . . . 9 ⊢ ((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ↔ ((TopOpen ↾ ∞MetSp) Fn ∞MetSp ∧ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top))
149	140, 147, 148	mpbir2an 702	. . . . . . . 8 ⊢ (TopOpen ↾ ∞MetSp):∞MetSp⟶Top
150		fco2 6296	. . . . . . . 8 ⊢ (((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen ∘ 𝑅):𝐼⟶Top)
151	149, 3, 150	sylancr 581	. . . . . . 7 ⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top)
152		eqid 2825	. . . . . . . 8 ⊢ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)
153	9, 152	ptbasfi 21755	. . . . . . 7 ⊢ ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅):𝐼⟶Top) → 𝐶 = (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))))
154	1, 151, 153	syl2anc 579	. . . . . 6 ⊢ (𝜑 → 𝐶 = (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))))
155		eqid 2825	. . . . . . . . 9 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
156	155	mopntop 22615	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top)
157	17, 156	syl 17	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘𝐷) ∈ Top)
158	13, 16, 14, 1, 4	prdsbas2 16482	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘)))
159	3, 72	sylan 575	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
160	3	ffvelrnda 6608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp)
161		xmstps 22628	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → (𝑅‘𝑘) ∈ TopSp)
162	160, 161	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ TopSp)
163	35, 71	istps 21109	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅‘𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉))
164	162, 163	sylib 210	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 ∈ (TopOn‘𝑉))
165	159, 164	eqeltrd 2906	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉))
166		toponuni 21089	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
167	165, 166	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑉 = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
168	35, 167	syl5eqr 2875	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (Base‘(𝑅‘𝑘)) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
169	168	ixpeq2dva 8190	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘)) = X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘))
170	158, 169	eqtrd 2861	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘))
171		fveq2 6433	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
172	171	unieqd 4668	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → ∪ ((TopOpen ∘ 𝑅)‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑛))
173	172	cbvixpv 8193	. . . . . . . . . . 11 ⊢ X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)
174	170, 173	syl6eq 2877	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛))
175	155	mopntopon 22614	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
176	17, 175	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
177		toponmax 21101	. . . . . . . . . . 11 ⊢ ((MetOpen‘𝐷) ∈ (TopOn‘𝐵) → 𝐵 ∈ (MetOpen‘𝐷))
178	176, 177	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (MetOpen‘𝐷))
179	174, 178	eqeltrrd 2907	. . . . . . . . 9 ⊢ (𝜑 → X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷))
180	179	snssd 4558	. . . . . . . 8 ⊢ (𝜑 → {X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷))
181	174	mpteq1d 4961	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
182	181	ad2antrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
183	182	cnveqd 5530	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
184	183	imaeq1d 5706	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))
185		fveq1 6432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑝 → (𝑤‘𝑘) = (𝑝‘𝑘))
186	185	eleq1d 2891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑝 → ((𝑤‘𝑘) ∈ 𝑢 ↔ (𝑝‘𝑘) ∈ 𝑢))
187		eqid 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘))
188	187	mptpreima 5869	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢}
189	186, 188	elrab2 3589	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))
190	160, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
191	190	adantr 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉))
192		simprl 787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ 𝐾)
193	160, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸))
194	193	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸))
195	192, 194	eleqtrd 2908	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸))
196		simprrr 800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → (𝑝‘𝑘) ∈ 𝑢)
197	54	mopni2 22668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
198	191, 195, 196, 197	syl3anc 1494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
199	17	ad3antrrr 721	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵))
200		simprrl 799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑝 ∈ 𝐵)
201	200	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ 𝐵)
202		rpxr 12123	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
203	202	ad2antrl 719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*)
204	155	blopn 22675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
205	199, 201, 203, 204	syl3anc 1494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
206		simprl 787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
207		blcntr 22588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
208	199, 201, 206, 207	syl3anc 1494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
209		blssm 22593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
210	199, 201, 203, 209	syl3anc 1494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
211		simplrr 796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
212		simplll 791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑)
213		rpgt0 12126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑟 ∈ ℝ+ → 0 < 𝑟)
214	213	ad2antrl 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟)
215	212, 201, 203, 214, 96	syl121anc 1498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
216	215	eleq2d 2892	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
217	216	biimpa 470	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
218		vex 3417	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑤 ∈ V
219	218	elixp 8182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟) ↔ (𝑤 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
220	219	simprbi 492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟) → ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
221	217, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
222		simp-4r 803	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘 ∈ 𝐼)
223		rsp 3138	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟) → (𝑘 ∈ 𝐼 → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
224	221, 222, 223	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
225	211, 224	sseldd 3828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ 𝑢)
226	210, 225	ssrabdv 3906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢})
227	226, 188	syl6sseqr 3877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))
228		eleq2 2895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝 ∈ 𝑦 ↔ 𝑝 ∈ (𝑝(ball‘𝐷)𝑟)))
229		sseq1 3851	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
230	228, 229	anbi12d 624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
231	230	rspcev 3526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
232	205, 208, 227, 231	syl12anc 870	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
233	198, 232	rexlimddv 3245	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
234	233	expr 450	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
235	189, 234	syl5bi 234	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
236	235	ralrimiv 3174	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
237	157	ad2antrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (MetOpen‘𝐷) ∈ Top)
238		eltop2 21150	. . . . . . . . . . . . . . . . 17 ⊢ ((MetOpen‘𝐷) ∈ Top → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
239	237, 238	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
240	236, 239	mpbird 249	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
241	184, 240	eqeltrrd 2907	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
242	241	ralrimiva 3175	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
243	159	raleqdv 3356	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)))
244	242, 243	mpbird 249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
245	244	ralrimiva 3175	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
246		fveq2 6433	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚))
247		fveq2 6433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑚 → (𝑤‘𝑘) = (𝑤‘𝑚))
248	247	mpteq2dv 4968	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑚 → (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)))
249	248	cnveqd 5530	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑚 → ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)))
250	249	imaeq1d 5706	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑚 → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))
251	250	eleq1d 2891	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → ((◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
252	246, 251	raleqbidv 3364	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
253	252	cbvralv 3383	. . . . . . . . . . 11 ⊢ (∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
254	245, 253	sylib 210	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
255		eqid 2825	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) = (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))
256	255	fmpt2x 7499	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
257	254, 256	sylib 210	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
258	257	frnd 6285	. . . . . . . 8 ⊢ (𝜑 → ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
259	180, 258	unssd 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‘𝐷)))
261	157, 259, 260	syl2anc 579	. . . . . 6 ⊢ (𝜑 → (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
262	154, 261	eqsstrd 3864	. . . . 5 ⊢ (𝜑 → 𝐶 ⊆ (fi‘(MetOpen‘𝐷)))
263		fitop 21075	. . . . . . 7 ⊢ ((MetOpen‘𝐷) ∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
264	157, 263	syl 17	. . . . . 6 ⊢ (𝜑 → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
265	155	mopnval 22613	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
266	17, 265	syl 17	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
267		tgdif0 21167	. . . . . . 7 ⊢ (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran (ball‘𝐷))
268	266, 267	syl6eqr 2879	. . . . . 6 ⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
269	264, 268	eqtrd 2861	. . . . 5 ⊢ (𝜑 → (fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
270	262, 269	sseqtrd 3866	. . . 4 ⊢ (𝜑 → 𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅})))
271		2basgen 21165	. . . 4 ⊢ (((ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅}))) → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
272	137, 270, 271	syl2anc 579	. . 3 ⊢ (𝜑 → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
273	11, 272	eqtr4d 2864	. 2 ⊢ (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
274		prdsxms.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝑌)
275	13, 14, 1, 4, 274	prdstopn 21802	. 2 ⊢ (𝜑 → 𝐽 = (∏t‘(TopOpen ∘ 𝑅)))
276	273, 275, 268	3eqtr4d 2871	1 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))

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  X_scprds 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