Theorem prdsxmslem2 23885

Description: Lemma for prdsxms 23886. 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 17307	. . . . 5 ⊢ TopOpen Fn V
3		prdsxms.r	. . . . . . 7 ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp)
4	3	ffnd 6669	. . . . . 6 ⊢ (𝜑 → 𝑅 Fn 𝐼)
5		dffn2 6670	. . . . . 6 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V)
6	4, 5	sylib 217	. . . . 5 ⊢ (𝜑 → 𝑅:𝐼⟶V)
7		fnfco 6707	. . . . 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 22921	. . . 4 ⊢ ((𝐼 ∈ Fin ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
11	1, 8, 10	syl2anc 584	. . 3 ⊢ (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶))
12		eldifsn 4747	. . . . . . . 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 23884	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
18		blrn 23762	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
19	17, 18	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟)))
20	17	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵))
21		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑝 ∈ 𝐵)
22		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑟 ∈ ℝ*)
23		xbln0 23767	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
24	20, 21, 22, 23	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
25	1	3ad2ant1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐼 ∈ Fin)
26	25	mptexd 7174	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V)
27		ovex 7390	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V
28	27	rgenw 3068	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑛 ∈ 𝐼 ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V
29		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))
30	29	fnmpt 6641	. . . . . . . . . . . . . . . . . 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 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅:𝐼⟶∞MetSp)
33	32	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp)
34		prdsxms.v	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑉 = (Base‘(𝑅‘𝑘))
35		prdsxms.e	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉))
36	34, 35	xmsxmet 23809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉))
37	33, 36	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
38		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
39		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
40	14	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑆 ∈ 𝑊)
41	33	ralrimiva 3143	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 (𝑅‘𝑘) ∈ ∞MetSp)
42		simp2l 1199	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ 𝐵)
43	32	feqmptd 6910	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
44	43	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
45	13, 44	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))
46	45	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
47	16, 46	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
48	42, 47	eleqtrd 2840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))
49	38, 39, 40, 25, 41, 34, 48	prdsbascl 17365	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 (𝑝‘𝑘) ∈ 𝑉)
50	49	r19.21bi 3234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑝‘𝑘) ∈ 𝑉)
51		simp2r 1200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑟 ∈ ℝ*)
52	51	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝑟 ∈ ℝ*)
53		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (MetOpen‘𝐸) = (MetOpen‘𝐸)
54	53	blopn 23856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝‘𝑘) ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
55	37, 50, 52, 54	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸))
56		2fveq3 6847	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → (dist‘(𝑅‘𝑛)) = (dist‘(𝑅‘𝑘)))
57		2fveq3 6847	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = (Base‘(𝑅‘𝑘)))
58	57, 34	eqtr4di 2794	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = 𝑉)
59	58	sqxpeqd 5665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))) = (𝑉 × 𝑉))
60	56, 59	reseq12d 5938	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉)))
61	60, 35	eqtr4di 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = 𝐸)
62	61	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))))) = (ball‘𝐸))
63		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (𝑝‘𝑛) = (𝑝‘𝑘))
64		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → 𝑟 = 𝑟)
65	62, 63, 64	oveq123d 7378	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
66		ovex 7390	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ V
67	65, 29, 66	fvmpt 6948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐼 → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
68	67	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
69		fvco3 6940	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘)))
70		prdsxms.k	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐾 = (TopOpen‘(𝑅‘𝑘))
71	69, 70	eqtr4di 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
72	32, 71	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
73	70, 34, 35	xmstopn 23804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸))
74	33, 73	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸))
75	72, 74	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸))
76	55, 68, 75	3eltr4d 2853	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
77	76	ralrimiva 3143	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))
78	32	feqmptd 6910	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑅 = (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))
79	78	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
80	13, 79	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑌 = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
81	80	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
82	15, 81	eqtrid 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
83	82	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))))
84	83	oveqd 7374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟))
85		fveq2 6842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝑅‘𝑛) = (𝑅‘𝑘))
86	85	cbvmptv 5218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)) = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))
87	86	oveq2i 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))
88		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
89		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))
90	80	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
91	16, 90	eqtrid 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
92	42, 91	eleqtrd 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))
93		simp3 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → 0 < 𝑟)
94	87, 88, 34, 35, 89, 40, 25, 33, 37, 92, 51, 93	prdsbl 23847	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
95	84, 94	eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
96		fneq1 6593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (𝑔 Fn 𝐼 ↔ (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼))
97		fveq1 6841	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (𝑔‘𝑘) = ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘))
98	97	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))
99	98	ralbidv 3174	. . . . . . . . . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟))
102	101	ixpeq2dva 8850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → X𝑘 ∈ 𝐼 (𝑔‘𝑘) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
103	102	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . 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 3556	. . . . . . . . . . . . . . . . . 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 1116	. . . . . . . . . . . . . . . . 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 1375	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 < 𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
108	107	3expia 1121	. . . . . . . . . . . . . . 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 3003	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ ↔ (𝑝(ball‘𝐷)𝑟) ≠ ∅))
113		df-3an 1089	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)))
114		ral0 4470	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)
115		difeq2 4076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = (𝐼 ∖ 𝐼))
116		difid 4330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐼 ∖ 𝐼) = ∅
117	115, 116	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = ∅)
118	117	raleqdv 3313	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)))
119	118	rspcev 3581	. . . . . . . . . . . . . . . . . . 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 289	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))))
124		eqeq1 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
125	123, 124	bi2anan9 637	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
126	125	exbidv 1924	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
127	110, 112, 126	3imtr4d 293	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
128	127	ex 413	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
129	128	rexlimdvva 3205	. . . . . . . . . 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	biimtrid 241	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
133	132	alrimiv 1930	. . . . . 6 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
134		ssab 4018	. . . . . 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 3995	. . . 4 ⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆ 𝐶)
137		ssv 3968	. . . . . . . . . 10 ⊢ ∞MetSp ⊆ V
138		fnssres 6624	. . . . . . . . . 10 ⊢ ((TopOpen Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn ∞MetSp)
139	2, 137, 138	mp2an 690	. . . . . . . . 9 ⊢ (TopOpen ↾ ∞MetSp) Fn ∞MetSp
140		fvres 6861	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) = (TopOpen‘𝑥))
141		xmstps 23806	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∞MetSp → 𝑥 ∈ TopSp)
142		eqid 2736	. . . . . . . . . . . . 13 ⊢ (TopOpen‘𝑥) = (TopOpen‘𝑥)
143	142	tpstop 22286	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ TopSp → (TopOpen‘𝑥) ∈ Top)
144	141, 143	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∞MetSp → (TopOpen‘𝑥) ∈ Top)
145	140, 144	eqeltrd 2838	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∞MetSp → ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top)
146	145	rgen 3066	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top
147		ffnfv 7066	. . . . . . . . 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 6695	. . . . . . . 8 ⊢ (((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen ∘ 𝑅):𝐼⟶Top)
150	148, 3, 149	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top)
151		eqid 2736	. . . . . . . 8 ⊢ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)
152	9, 151	ptbasfi 22932	. . . . . . 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 2736	. . . . . . . . 9 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
155	154	mopntop 23793	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top)
156	17, 155	syl 17	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘𝐷) ∈ Top)
157	13, 16, 14, 1, 4	prdsbas2 17351	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘)))
158	3, 71	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾)
159	3	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp)
160		xmstps 23806	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑘) ∈ ∞MetSp → (𝑅‘𝑘) ∈ TopSp)
161	159, 160	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ TopSp)
162	34, 70	istps 22283	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅‘𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉))
163	161, 162	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 ∈ (TopOn‘𝑉))
164	158, 163	eqeltrd 2838	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉))
165		toponuni 22263	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
166	164, 165	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑉 = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
167	34, 166	eqtr3id 2790	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (Base‘(𝑅‘𝑘)) = ∪ ((TopOpen ∘ 𝑅)‘𝑘))
168	167	ixpeq2dva 8850	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘)) = X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘))
169	157, 168	eqtrd 2776	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘))
170		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛))
171	170	unieqd 4879	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → ∪ ((TopOpen ∘ 𝑅)‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑛))
172	171	cbvixpv 8853	. . . . . . . . . . 11 ⊢ X𝑘 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)
173	169, 172	eqtrdi 2792	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛))
174	154	mopntopon 23792	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
175	17, 174	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵))
176		toponmax 22275	. . . . . . . . . . 11 ⊢ ((MetOpen‘𝐷) ∈ (TopOn‘𝐵) → 𝐵 ∈ (MetOpen‘𝐷))
177	175, 176	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (MetOpen‘𝐷))
178	173, 177	eqeltrrd 2839	. . . . . . . . 9 ⊢ (𝜑 → X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷))
179	178	snssd 4769	. . . . . . . 8 ⊢ (𝜑 → {X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷))
180	173	mpteq1d 5200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
181	180	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
182	181	cnveqd 5831	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)))
183	182	imaeq1d 6012	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))
184		fveq1 6841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑝 → (𝑤‘𝑘) = (𝑝‘𝑘))
185	184	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑝 → ((𝑤‘𝑘) ∈ 𝑢 ↔ (𝑝‘𝑘) ∈ 𝑢))
186		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘))
187	186	mptpreima 6190	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢}
188	185, 187	elrab2 3648	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))
189	159, 36	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
190	189	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉))
191		simprl 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ 𝐾)
192	159, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸))
193	192	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸))
194	191, 193	eleqtrd 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸))
195		simprrr 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → (𝑝‘𝑘) ∈ 𝑢)
196	53	mopni2 23849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
197	190, 194, 195, 196	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
198	17	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵))
199		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑝 ∈ 𝐵)
200	199	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ 𝐵)
201		rpxr 12924	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
202	201	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*)
203	154	blopn 23856	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
204	198, 200, 202, 203	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷))
205		simprl 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
206		blcntr 23766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
207	198, 200, 205, 206	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))
208		blssm 23771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
209	198, 200, 202, 208	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵)
210		simplrr 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)
211		simplll 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑)
212		rpgt0 12927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑟 ∈ ℝ+ → 0 < 𝑟)
213	212	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟)
214	211, 200, 202, 213, 95	syl121anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
215	214	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
216	215	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))
217		vex 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑤 ∈ V
218	217	elixp 8842	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘 ∈ 𝐼)
222		rsp 3230	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟) → (𝑘 ∈ 𝐼 → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)))
223	220, 221, 222	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))
224	210, 223	sseldd 3945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ 𝑢)
225	209, 224	ssrabdv 4031	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢})
226	225, 187	sseqtrrdi 3995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))
227		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝 ∈ 𝑦 ↔ 𝑝 ∈ (𝑝(ball‘𝐷)𝑟)))
228		sseq1 3969	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
229	227, 228	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
230	229	rspcev 3581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
231	204, 207, 226, 230	syl12anc 835	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
232	197, 231	rexlimddv 3158	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
233	232	expr 457	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
234	188, 233	biimtrid 241	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
235	234	ralrimiv 3142	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))
236	156	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (MetOpen‘𝐷) ∈ Top)
237		eltop2 22325	. . . . . . . . . . . . . . . . 17 ⊢ ((MetOpen‘𝐷) ∈ Top → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
238	236, 237	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))))
239	235, 238	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
240	183, 239	eqeltrrd 2839	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
241	240	ralrimiva 3143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
242	158	raleqdv 3313	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)))
243	241, 242	mpbird 256	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
244	243	ralrimiva 3143	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))
245		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚))
246		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑚 → (𝑤‘𝑘) = (𝑤‘𝑚))
247	246	mpteq2dv 5207	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑚 → (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)))
248	247	cnveqd 5831	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑚 → ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)))
249	248	imaeq1d 6012	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑚 → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))
250	249	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → ((◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
251	245, 250	raleqbidv 3319	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)))
252	251	cbvralvw 3225	. . . . . . . . . . 11 ⊢ (∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
253	244, 252	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))
254		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) = (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))
255	254	fmpox 7999	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
256	253, 255	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷))
257	256	frnd 6676	. . . . . . . 8 ⊢ (𝜑 → ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷))
258	179, 257	unssd 4146	. . . . . . 7 ⊢ (𝜑 → ({X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷))
259		fiss 9360	. . . . . . 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 3982	. . . . 5 ⊢ (𝜑 → 𝐶 ⊆ (fi‘(MetOpen‘𝐷)))
262		fitop 22249	. . . . . . 7 ⊢ ((MetOpen‘𝐷) ∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
263	156, 262	syl 17	. . . . . 6 ⊢ (𝜑 → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷))
264	154	mopnval 23791	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
265	17, 264	syl 17	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘ran (ball‘𝐷)))
266		tgdif0 22342	. . . . . . 7 ⊢ (topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran (ball‘𝐷))
267	265, 266	eqtr4di 2794	. . . . . 6 ⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
268	263, 267	eqtrd 2776	. . . . 5 ⊢ (𝜑 → (fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
269	261, 268	sseqtrd 3984	. . . 4 ⊢ (𝜑 → 𝐶 ⊆ (topGen‘(ran (ball‘𝐷) ∖ {∅})))
270		2basgen 22340	. . . 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 2779	. 2 ⊢ (𝜑 → (∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖ {∅})))
273		prdsxms.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝑌)
274	13, 14, 1, 4, 273	prdstopn 22979	. 2 ⊢ (𝜑 → 𝐽 = (∏t‘(TopOpen ∘ 𝑅)))
275	272, 274, 267	3eqtr4d 2786	1 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  {crab 3407  Vcvv 3445   ∖ cdif 3907   ∪ cun 3908   ⊆ wss 3910  ∅c0 4282  {csn 4586  ∪ cuni 4865  ∪ ciun 4954   class class class wbr 5105   ↦ cmpt 5188   × cxp 5631  ^◡ccnv 5632  ran crn 5634   ↾ cres 5635   “ cima 5636   ∘ ccom 5637   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357   ∈ cmpo 7359  Xcixp 8835  Fincfn 8883  ficfi 9346  0cc0 11051  ℝ^*cxr 11188   < clt 11189  ℝ⁺crp 12915  Basecbs 17083  distcds 17142  TopOpenctopn 17303  topGenctg 17319  ∏_tcpt 17320  X_scprds 17327  ∞Metcxmet 20781  ballcbl 20783  MetOpencmopn 20786  Topctop 22242  TopOnctopon 22259  TopSpctps 22281  ∞MetSpcxms 23670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-icc 13271  df-fz 13425  df-struct 17019  df-slot 17054  df-ndx 17066  df-base 17084  df-plusg 17146  df-mulr 17147  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-topgen 17325  df-pt 17326  df-prds 17329  df-psmet 20788  df-xmet 20789  df-bl 20791  df-mopn 20792  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-xms 23673

This theorem is referenced by:  prdsxms  23886