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.

Step	Hyp	Ref	Expression
1		prdsxms.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ Fin)
2		topnfn 17145	. . . . 5 ⊢ TopOpen Fn V
3		prdsxms.r	. . . . . . 7 ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp)
4	3	ffnd 6610	. . . . . 6 ⊢ (𝜑 → 𝑅 Fn 𝐼)
5		dffn2 6611	. . . . . 6 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V)
6	4, 5	sylib 217	. . . . 5 ⊢ (𝜑 → 𝑅:𝐼⟶V)
7		fnfco 6648	. . . . 5 ⊢ ((TopOpen Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen ∘ 𝑅) Fn 𝐼)
8	2, 6, 7	sylancr 587	. . . 4 ⊢ (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼)
9		prdsxms.c	. . . . 5 ⊢ 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))}
10	9	ptval 22730	. . . 4 ⊢ ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
11	1, 8, 10	syl2anc 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‘𝑌)
17	13, 14, 1, 15, 16, 3	prdsxmslem1 23693	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
18		blrn 23571	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
19	17, 18	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
20	17	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵))
21		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑝 ∈ 𝐵)
22		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑟 ∈ ℝ*)
23		xbln0 23576	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
24	20, 21, 22, 23	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
25	1	3ad2ant1 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐼 ∈ Fin)
26	25	mptexd 7109	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V)
27		ovex 7317	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V
28	27	rgenw 3077	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑛 ∈ 𝐼 ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V
29		eqid 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))
30	29	fnmpt 6582	. . . . . . . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅:𝐼⟶∞MetSp)
33	32	ffvelrnda 6970	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp)
34		prdsxms.v	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑉 = (Base‘(𝑅‘𝑘))
35		prdsxms.e	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉))
36	34, 35	xmsxmet 23618	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉))
37	33, 36	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
38		eqid 2739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
39		eqid 2739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
40	14	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑆 ∈ 𝑊)
41	33	ralrimiva 3104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 (𝑅‘𝑘) ∈ ∞MetSp)
42		simp2l 1198	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ 𝐵)
43	32	feqmptd 6846	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
44	43	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
45	13, 44	eqtrid 2791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
46	45	fveq2d 6787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
47	16, 46	eqtrid 2791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
48	42, 47	eleqtrd 2842	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
49	38, 39, 40, 25, 41, 34, 48	prdsbascl 17203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 (𝑝‘𝑘) ∈ 𝑉)
50	49	r19.21bi 3135	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑝‘𝑘) ∈ 𝑉)
51		simp2r 1199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑟 ∈ ℝ*)
52	51	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝑟 ∈ ℝ*)
53		eqid 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (MetOpen‘𝐸) = (MetOpen‘𝐸)
54	53	blopn 23665	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝‘𝑘) ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
55	37, 50, 52, 54	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
56		2fveq3 6788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → (dist‘(𝑅‘𝑛)) = (dist‘(𝑅‘𝑘)))
57		2fveq3 6788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = (Base‘(𝑅‘𝑘)))
58	57, 34	eqtr4di 2797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = 𝑉)
59	58	sqxpeqd 5622	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))) = (𝑉 × 𝑉))
60	56, 59	reseq12d 5895	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉)))
61	60, 35	eqtr4di 2797	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = 𝐸)
62	61	fveq2d 6787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))))) = (ball‘𝐸))
63		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (𝑝‘𝑛) = (𝑝‘𝑘))
64		eqidd 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → 𝑟 = 𝑟)
65	62, 63, 64	oveq123d 7305	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
66		ovex 7317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ V
67	65, 29, 66	fvmpt 6884	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐼 → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
68	67	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
69		fvco3 6876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘)))
70		prdsxms.k	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐾 = (TopOpen‘(𝑅‘𝑘))
71	69, 70	eqtr4di 2797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
72	32, 71	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
73	70, 34, 35	xmstopn 23613	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸))
74	33, 73	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸))
75	72, 74	eqtrd 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸))
76	55, 68, 75	3eltr4d 2855	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
77	76	ralrimiva 3104	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
78	32	feqmptd 6846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))
79	78	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
80	13, 79	eqtrid 2791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
81	80	fveq2d 6787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
82	15, 81	eqtrid 2791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
83	82	fveq2d 6787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))))
84	83	oveqd 7301	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟))
85		fveq2 6783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝑅‘𝑛) = (𝑅‘𝑘))
86	85	cbvmptv 5188	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)) = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))
87	86	oveq2i 7295	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
88		eqid 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
89		eqid 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
90	80	fveq2d 6787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
91	16, 90	eqtrid 2791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
92	42, 91	eleqtrd 2842	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
93		simp3 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 0 < 𝑟)
94	87, 88, 34, 35, 89, 40, 25, 33, 37, 92, 51, 93	prdsbl 23656	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
95	84, 94	eqtrd 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‘(𝑅‘𝑛)))))𝑟))‘𝑘))
98	97	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
99	98	ralbidv 3113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
100	96, 99	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
101	97, 67	sylan9eq 2799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
102	101	ixpeq2dva 8709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → X𝑘 ∈ 𝐼 (𝑔‘𝑘) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
103	102	eqeq2d 2750	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
104	100, 103	anbi12d 631	. . . . . . . . . . . . . . . . . . 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 3537	. . . . . . . . . . . . . . . . . 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 1115	. . . . . . . . . . . . . . . . 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 1374	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
108	107	3expia 1120	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (0 < 𝑟 → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
109	24, 108	sylbid 239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
110	109	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
111		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → 𝑥 = (𝑝(ball‘𝐷)𝑟))
112	111	neeq1d 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 ⊢ (𝐼 ∖ 𝐼) = ∅
117	115, 116	eqtrdi 2795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = ∅)
118	117	raleqdv 3349	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)))
119	118	rspcev 3562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
120	1, 114, 119	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
121	120	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
122	121	biantrud 532	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))))
123	113, 122	bitr4id 290	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
124		eqeq1 2743	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
125	123, 124	bi2anan9 636	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
126	125	exbidv 1925	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
127	110, 112, 126	3imtr4d 294	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
128	127	ex 413	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
129	128	rexlimdvva 3224	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
130	19, 129	sylbid 239	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
131	130	impd 411	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
132	12, 131	syl5bi 241	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
133	132	alrimiv 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𝑘 ∈ 𝐼 (𝑔‘𝑘))))
135	133, 134	sylibr 233	. . . . 5 ⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))})
136	135, 9	sseqtrrdi 3973	. . . 4 ⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶)
137		ssv 3946	. . . . . . . . . 10 ⊢ ∞MetSp ⊆ V
138		fnssres 6564	. . . . . . . . . 10 ⊢ ((TopOpen Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn ∞MetSp)
139	2, 137, 138	mp2an 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‘𝑥)
143	142	tpstop 22095	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ TopSp → (TopOpen‘𝑥) ∈ Top)
144	141, 143	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∞MetSp → (TopOpen‘𝑥) ∈ Top)
145	140, 144	eqeltrd 2840	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top)
146	145	rgen 3075	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top
147		ffnfv 7001	. . . . . . . . 9 ⊢ ((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ↔ ((TopOpen ↾ ∞MetSp) Fn ∞MetSp ∧ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top))
148	139, 146, 147	mpbir2an 708	. . . . . . . 8 ⊢ (TopOpen ↾ ∞MetSp):∞MetSp⟶Top
149		fco2 6636	. . . . . . . 8 ⊢ (((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen ∘ 𝑅):𝐼⟶Top)
150	148, 3, 149	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top)
151		eqid 2739	. . . . . . . 8 ⊢ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)
152	9, 151	ptbasfi 22741	. . . . . . 7 ⊢ ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅):𝐼⟶Top) → 𝐶 = (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))))
153	1, 150, 152	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝐶 = (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))))
154		eqid 2739	. . . . . . . . 9 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
155	154	mopntop 23602	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top)
156	17, 155	syl 17	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘𝐷) ∈ Top)
157	13, 16, 14, 1, 4	prdsbas2 17189	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘)))
158	3, 71	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
159	3	ffvelrnda 6970	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp)
160		xmstps 23615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → (𝑅‘𝑘) ∈ TopSp)
161	159, 160	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ TopSp)
162	34, 70	istps 22092	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅‘𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉))
163	161, 162	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 ∈ (TopOn‘𝑉))
164	158, 163	eqeltrd 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉))
165		toponuni 22072	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
166	164, 165	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑉 = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
167	34, 166	eqtr3id 2793	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (Base‘(𝑅‘𝑘)) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
168	167	ixpeq2dva 8709	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘)) = X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘))
169	157, 168	eqtrd 2779	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘))
170		fveq2 6783	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
171	170	unieqd 4854	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → ∪ ((TopOpen ∘ 𝑅)‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑛))
172	171	cbvixpv 8712	. . . . . . . . . . 11 ⊢ X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)
173	169, 172	eqtrdi 2795	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛))
174	154	mopntopon 23601	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
175	17, 174	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
176		toponmax 22084	. . . . . . . . . . 11 ⊢ ((MetOpen‘𝐷) ∈ (TopOn‘𝐵) → 𝐵 ∈ (MetOpen‘𝐷))
177	175, 176	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (MetOpen‘𝐷))
178	173, 177	eqeltrrd 2841	. . . . . . . . 9 ⊢ (𝜑 → X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷))
179	178	snssd 4743	. . . . . . . 8 ⊢ (𝜑 → {X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷))
180	173	mpteq1d 5170	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
181	180	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
182	181	cnveqd 5787	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
183	182	imaeq1d 5971	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))
184		fveq1 6782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑝 → (𝑤‘𝑘) = (𝑝‘𝑘))
185	184	eleq1d 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑝 → ((𝑤‘𝑘) ∈ 𝑢 ↔ (𝑝‘𝑘) ∈ 𝑢))
186		eqid 2739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘))
187	186	mptpreima 6146	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢}
188	185, 187	elrab2 3628	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))
189	159, 36	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
190	189	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉))
191		simprl 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ 𝐾)
192	159, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸))
193	192	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸))
194	191, 193	eleqtrd 2842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸))
195		simprrr 779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → (𝑝‘𝑘) ∈ 𝑢)
196	53	mopni2 23658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
197	190, 194, 195, 196	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
198	17	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵))
199		simprrl 778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑝 ∈ 𝐵)
200	199	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ 𝐵)
201		rpxr 12748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
202	201	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*)
203	154	blopn 23665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
204	198, 200, 202, 203	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
205		simprl 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
206		blcntr 23575	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
207	198, 200, 205, 206	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
208		blssm 23580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
209	198, 200, 202, 208	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
210		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
211		simplll 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑)
212		rpgt0 12751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑟 ∈ ℝ+ → 0 < 𝑟)
213	212	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟)
214	211, 200, 202, 213, 95	syl121anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
215	214	eleq2d 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
216	215	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
217		vex 3437	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑤 ∈ V
218	217	elixp 8701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟) ↔ (𝑤 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
219	218	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟) → ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
220	216, 219	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
221		simp-4r 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘 ∈ 𝐼)
222		rsp 3132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟) → (𝑘 ∈ 𝐼 → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
223	220, 221, 222	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
224	210, 223	sseldd 3923	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ 𝑢)
225	209, 224	ssrabdv 4008	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢})
226	225, 187	sseqtrrdi 3973	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))
227		eleq2 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝 ∈ 𝑦 ↔ 𝑝 ∈ (𝑝(ball‘𝐷)𝑟)))
228		sseq1 3947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
229	227, 228	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
230	229	rspcev 3562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
231	204, 207, 226, 230	syl12anc 834	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
232	197, 231	rexlimddv 3221	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
233	232	expr 457	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
234	188, 233	syl5bi 241	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
235	234	ralrimiv 3103	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
236	156	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (MetOpen‘𝐷) ∈ Top)
237		eltop2 22134	. . . . . . . . . . . . . . . . 17 ⊢ ((MetOpen‘𝐷) ∈ Top → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
238	236, 237	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
239	235, 238	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
240	183, 239	eqeltrrd 2841	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
241	240	ralrimiva 3104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
242	158	raleqdv 3349	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)))
243	241, 242	mpbird 256	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
244	243	ralrimiva 3104	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
245		fveq2 6783	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚))
246		fveq2 6783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑚 → (𝑤‘𝑘) = (𝑤‘𝑚))
247	246	mpteq2dv 5177	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑚 → (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)))
248	247	cnveqd 5787	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑚 → ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)))
249	248	imaeq1d 5971	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑚 → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))
250	249	eleq1d 2824	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → ((◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
251	245, 250	raleqbidv 3337	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
252	251	cbvralvw 3384	. . . . . . . . . . 11 ⊢ (∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
253	244, 252	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
254		eqid 2739	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) = (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))
255	254	fmpox 7916	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
256	253, 255	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
257	256	frnd 6617	. . . . . . . 8 ⊢ (𝜑 → ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
258	179, 257	unssd 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‘𝐷)))
260	156, 258, 259	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷)))
261	153, 260	eqsstrd 3960	. . . . 5 ⊢ (𝜑 → 𝐶 ⊆ (fi‘(MetOpen‘𝐷)))
262		fitop 22058	. . . . . . 7 ⊢ ((MetOpen‘𝐷) ∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
263	156, 262	syl 17	. . . . . 6 ⊢ (𝜑 → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
264	154	mopnval 23600	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
265	17, 264	syl 17	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
266		tgdif0 22151	. . . . . . 7 ⊢ (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran (ball‘𝐷))
267	265, 266	eqtr4di 2797	. . . . . 6 ⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
268	263, 267	eqtrd 2779	. . . . 5 ⊢ (𝜑 → (fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
269	261, 268	sseqtrd 3962	. . . 4 ⊢ (𝜑 → 𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅})))
270		2basgen 22149	. . . 4 ⊢ (((ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅}))) → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
271	136, 269, 270	syl2anc 584	. . 3 ⊢ (𝜑 → (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶))
272	11, 271	eqtr4d 2782	. 2 ⊢ (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
273		prdsxms.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝑌)
274	13, 14, 1, 4, 273	prdstopn 22788	. 2 ⊢ (𝜑 → 𝐽 = (∏t‘(TopOpen ∘ 𝑅)))
275	272, 274, 267	3eqtr4d 2789	1 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))

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