prdsxmslem2

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

	Ref	Expression
Hypotheses	prdsxms.y	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
	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	prdsxmslem2	⊢ ( 𝜑 → 𝐽 = ( MetOpen ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		prdsxms.y	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
2		prdsxms.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
3		prdsxms.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
4		prdsxms.d	⊢ 𝐷 = ( dist ‘ 𝑌 )
5		prdsxms.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
6		prdsxms.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ ∞MetSp )
7		prdsxms.j	⊢ 𝐽 = ( TopOpen ‘ 𝑌 )
8		prdsxms.v	⊢ 𝑉 = ( Base ‘ ( 𝑅 ‘ 𝑘 ) )
9		prdsxms.e	⊢ 𝐸 = ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( 𝑉 × 𝑉 ) )
10		prdsxms.k	⊢ 𝐾 = ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) )
11		prdsxms.c	⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) }
12		topnfn	⊢ TopOpen Fn V
13	6	ffnd	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
14		dffn2	⊢ ( 𝑅 Fn 𝐼 ↔ 𝑅 : 𝐼 ⟶ V )
15	13 14	sylib	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ V )
16		fnfco	⊢ ( ( TopOpen Fn V ∧ 𝑅 : 𝐼 ⟶ V ) → ( TopOpen ∘ 𝑅 ) Fn 𝐼 )
17	12 15 16	sylancr	⊢ ( 𝜑 → ( TopOpen ∘ 𝑅 ) Fn 𝐼 )
18	11	ptval	⊢ ( ( 𝐼 ∈ Fin ∧ ( TopOpen ∘ 𝑅 ) Fn 𝐼 ) → ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ 𝐶 ) )
19	3 17 18	syl2anc	⊢ ( 𝜑 → ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ 𝐶 ) )
20		eldifsn	⊢ ( 𝑥 ∈ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ↔ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑥 ≠ ∅ ) )
21	1 2 3 4 5 6	prdsxmslem1	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
22		blrn	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ↔ ∃ 𝑝 ∈ 𝐵 ∃ 𝑟 ∈ ℝ^* 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) )
23	21 22	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ↔ ∃ 𝑝 ∈ 𝐵 ∃ 𝑟 ∈ ℝ^* 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) )
24	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
25		simprl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → 𝑝 ∈ 𝐵 )
26		simprr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → 𝑟 ∈ ℝ^* )
27		xbln0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ ↔ 0 < 𝑟 ) )
28	24 25 26 27	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ ↔ 0 < 𝑟 ) )
29	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝐼 ∈ Fin )
30	29	mptexd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ∈ V )
31		ovex	⊢ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ∈ V
32	31	rgenw	⊢ ∀ 𝑛 ∈ 𝐼 ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ∈ V
33		eqid	⊢ ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) )
34	33	fnmpt	⊢ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ∈ V → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 )
35	32 34	mp1i	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 )
36	6	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑅 : 𝐼 ⟶ ∞MetSp )
37	36	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp )
38	8 9	xmsxmet	⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
39	37 38	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
40		eqid	⊢ ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) = ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
41		eqid	⊢ ( Base ‘ ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( Base ‘ ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
42	2	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑆 ∈ 𝑊 )
43	37	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp )
44		simp2l	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ 𝐵 )
45	36	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑅 = ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
46	45	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( 𝑆 X_s 𝑅 ) = ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
47	1 46	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑌 = ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
48	47	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
49	5 48	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝐵 = ( Base ‘ ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
50	44 49	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ ( Base ‘ ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
51	40 41 42 29 43 8 50	prdsbascl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( 𝑝 ‘ 𝑘 ) ∈ 𝑉 )
52	51	r19.21bi	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑝 ‘ 𝑘 ) ∈ 𝑉 )
53		simp2r	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑟 ∈ ℝ^* )
54	53	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑟 ∈ ℝ^* )
55		eqid	⊢ ( MetOpen ‘ 𝐸 ) = ( MetOpen ‘ 𝐸 )
56	55	blopn	⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑉 ∧ 𝑟 ∈ ℝ^* ) → ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐸 ) )
57	39 52 54 56	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐸 ) )
58		2fveq3	⊢ ( 𝑛 = 𝑘 → ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) = ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) )
59		2fveq3	⊢ ( 𝑛 = 𝑘 → ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) )
60	59 8	eqtr4di	⊢ ( 𝑛 = 𝑘 → ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) = 𝑉 )
61	60	sqxpeqd	⊢ ( 𝑛 = 𝑘 → ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) = ( 𝑉 × 𝑉 ) )
62	58 61	reseq12d	⊢ ( 𝑛 = 𝑘 → ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) = ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( 𝑉 × 𝑉 ) ) )
63	62 9	eqtr4di	⊢ ( 𝑛 = 𝑘 → ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) = 𝐸 )
64	63	fveq2d	⊢ ( 𝑛 = 𝑘 → ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) = ( ball ‘ 𝐸 ) )
65		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑝 ‘ 𝑛 ) = ( 𝑝 ‘ 𝑘 ) )
66		eqidd	⊢ ( 𝑛 = 𝑘 → 𝑟 = 𝑟 )
67	64 65 66	oveq123d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) = ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
68		ovex	⊢ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ V
69	67 33 68	fvmpt	⊢ ( 𝑘 ∈ 𝐼 → ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) = ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
70	69	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) = ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
71		fvco3	⊢ ( ( 𝑅 : 𝐼 ⟶ ∞MetSp ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) )
72	71 10	eqtr4di	⊢ ( ( 𝑅 : 𝐼 ⟶ ∞MetSp ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = 𝐾 )
73	36 72	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = 𝐾 )
74	10 8 9	xmstopn	⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp → 𝐾 = ( MetOpen ‘ 𝐸 ) )
75	37 74	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐾 = ( MetOpen ‘ 𝐸 ) )
76	73 75	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( MetOpen ‘ 𝐸 ) )
77	57 70 76	3eltr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
78	77	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
79	36	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑅 = ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) )
80	79	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( 𝑆 X_s 𝑅 ) = ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) )
81	1 80	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑌 = ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) )
82	81	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
83	4 82	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝐷 = ( dist ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
84	83	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( ball ‘ 𝐷 ) = ( ball ‘ ( dist ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) )
85	84	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑝 ( ball ‘ ( dist ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) )
86		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑅 ‘ 𝑛 ) = ( 𝑅 ‘ 𝑘 ) )
87	86	cbvmptv	⊢ ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) )
88	87	oveq2i	⊢ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) = ( 𝑆 X_s ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
89		eqid	⊢ ( Base ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) = ( Base ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) )
90		eqid	⊢ ( dist ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) = ( dist ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) )
91	81	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
92	5 91	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝐵 = ( Base ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
93	44 92	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ ( Base ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
94		simp3	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → 0 < 𝑟 )
95	88 89 8 9 90 42 29 37 39 93 53 94	prdsbl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( 𝑝 ( ball ‘ ( dist ‘ ( 𝑆 X_s ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
96	85 95	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
97		fneq1	⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( 𝑔 Fn 𝐼 ↔ ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ) )
98		fveq1	⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( 𝑔 ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) )
99	98	eleq1d	⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ↔ ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
100	99	ralbidv	⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
101	97 100	anbi12d	⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ↔ ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) )
102	98 69	sylan9eq	⊢ ( ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑘 ) = ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
103	102	ixpeq2dva	⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
104	103	eqeq2d	⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ↔ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
105	101 104	anbi12d	⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ↔ ( ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
106	105	spcegv	⊢ ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( 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	⊢ ( ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ∈ V ∧ ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) )
108	30 35 78 96 107	syl121anc	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ∧ 0 < 𝑟 ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) )
109	108	3expia	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → ( 0 < 𝑟 → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
110	28 109	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
111	110	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
112		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) )
113	112	neeq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝑥 ≠ ∅ ↔ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ ) )
114		df-3an	⊢ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ↔ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
115		ral0	⊢ ∀ 𝑘 ∈ ∅ ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 )
116		difeq2	⊢ ( 𝑧 = 𝐼 → ( 𝐼 ∖ 𝑧 ) = ( 𝐼 ∖ 𝐼 ) )
117		difid	⊢ ( 𝐼 ∖ 𝐼 ) = ∅
118	116 117	eqtrdi	⊢ ( 𝑧 = 𝐼 → ( 𝐼 ∖ 𝑧 ) = ∅ )
119	118	raleqdv	⊢ ( 𝑧 = 𝐼 → ( ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ∅ ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
120	119	rspcev	⊢ ( ( 𝐼 ∈ Fin ∧ ∀ 𝑘 ∈ ∅ ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) → ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
121	3 115 120	sylancl	⊢ ( 𝜑 → ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
122	121	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
123	122	biantrud	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ↔ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) )
124	114 123	bitr4id	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ↔ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) )
125		eqeq1	⊢ ( 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ↔ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) )
126	124 125	bi2anan9	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ↔ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
127	126	exbidv	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
128	111 113 127	3imtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝑥 ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
129	128	ex	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) ) → ( 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑥 ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) )
130	129	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝐵 ∃ 𝑟 ∈ ℝ^* 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑥 ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) )
131	23 130	sylbid	⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) → ( 𝑥 ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) )
132	131	impd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
133	20 132	biimtrid	⊢ ( 𝜑 → ( 𝑥 ∈ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
134	133	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
135		ssab	⊢ ( ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) } ↔ ∀ 𝑥 ( 𝑥 ∈ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) )
136	134 135	sylibr	⊢ ( 𝜑 → ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) } )
137	136 11	sseqtrrdi	⊢ ( 𝜑 → ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ 𝐶 )
138		ssv	⊢ ∞MetSp ⊆ V
139		fnssres	⊢ ( ( TopOpen Fn V ∧ ∞MetSp ⊆ V ) → ( TopOpen ↾ ∞MetSp ) Fn ∞MetSp )
140	12 138 139	mp2an	⊢ ( TopOpen ↾ ∞MetSp ) Fn ∞MetSp
141		fvres	⊢ ( 𝑥 ∈ ∞MetSp → ( ( TopOpen ↾ ∞MetSp ) ‘ 𝑥 ) = ( TopOpen ‘ 𝑥 ) )
142		xmstps	⊢ ( 𝑥 ∈ ∞MetSp → 𝑥 ∈ TopSp )
143		eqid	⊢ ( TopOpen ‘ 𝑥 ) = ( TopOpen ‘ 𝑥 )
144	143	tpstop	⊢ ( 𝑥 ∈ TopSp → ( TopOpen ‘ 𝑥 ) ∈ Top )
145	142 144	syl	⊢ ( 𝑥 ∈ ∞MetSp → ( TopOpen ‘ 𝑥 ) ∈ Top )
146	141 145	eqeltrd	⊢ ( 𝑥 ∈ ∞MetSp → ( ( TopOpen ↾ ∞MetSp ) ‘ 𝑥 ) ∈ Top )
147	146	rgen	⊢ ∀ 𝑥 ∈ ∞MetSp ( ( TopOpen ↾ ∞MetSp ) ‘ 𝑥 ) ∈ Top
148		ffnfv	⊢ ( ( TopOpen ↾ ∞MetSp ) : ∞MetSp ⟶ Top ↔ ( ( TopOpen ↾ ∞MetSp ) Fn ∞MetSp ∧ ∀ 𝑥 ∈ ∞MetSp ( ( TopOpen ↾ ∞MetSp ) ‘ 𝑥 ) ∈ Top ) )
149	140 147 148	mpbir2an	⊢ ( TopOpen ↾ ∞MetSp ) : ∞MetSp ⟶ Top
150		fco2	⊢ ( ( ( TopOpen ↾ ∞MetSp ) : ∞MetSp ⟶ Top ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
151	149 6 150	sylancr	⊢ ( 𝜑 → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
152		eqid	⊢ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) = X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 )
153	11 152	ptbasfi	⊢ ( ( 𝐼 ∈ Fin ∧ ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top ) → 𝐶 = ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) )
154	3 151 153	syl2anc	⊢ ( 𝜑 → 𝐶 = ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) )
155		eqid	⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
156	155	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ 𝐷 ) ∈ Top )
157	21 156	syl	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) ∈ Top )
158	1 5 2 3 13	prdsbas2	⊢ ( 𝜑 → 𝐵 = X 𝑘 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) )
159	6 72	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = 𝐾 )
160	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp )
161		xmstps	⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp → ( 𝑅 ‘ 𝑘 ) ∈ TopSp )
162	160 161	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ TopSp )
163	8 10	istps	⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ 𝑉 ) )
164	162 163	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐾 ∈ ( TopOn ‘ 𝑉 ) )
165	159 164	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∈ ( TopOn ‘ 𝑉 ) )
166		toponuni	⊢ ( ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∈ ( TopOn ‘ 𝑉 ) → 𝑉 = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
167	165 166	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑉 = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
168	8 167	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
169	168	ixpeq2dva	⊢ ( 𝜑 → X 𝑘 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) = X 𝑘 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
170	158 169	eqtrd	⊢ ( 𝜑 → 𝐵 = X 𝑘 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) )
171		fveq2	⊢ ( 𝑘 = 𝑛 → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) )
172	171	unieqd	⊢ ( 𝑘 = 𝑛 → ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) )
173	172	cbvixpv	⊢ X 𝑘 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 )
174	170 173	eqtrdi	⊢ ( 𝜑 → 𝐵 = X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) )
175	155	mopntopon	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ 𝐷 ) ∈ ( TopOn ‘ 𝐵 ) )
176	21 175	syl	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) ∈ ( TopOn ‘ 𝐵 ) )
177		toponmax	⊢ ( ( MetOpen ‘ 𝐷 ) ∈ ( TopOn ‘ 𝐵 ) → 𝐵 ∈ ( MetOpen ‘ 𝐷 ) )
178	176 177	syl	⊢ ( 𝜑 → 𝐵 ∈ ( MetOpen ‘ 𝐷 ) )
179	174 178	eqeltrrd	⊢ ( 𝜑 → X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ∈ ( MetOpen ‘ 𝐷 ) )
180	179	snssd	⊢ ( 𝜑 → { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ⊆ ( MetOpen ‘ 𝐷 ) )
181	174	mpteq1d	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) )
182	181	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) )
183	182	cnveqd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) = ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) )
184	183	imaeq1d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
185		fveq1	⊢ ( 𝑤 = 𝑝 → ( 𝑤 ‘ 𝑘 ) = ( 𝑝 ‘ 𝑘 ) )
186	185	eleq1d	⊢ ( 𝑤 = 𝑝 → ( ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) )
187		eqid	⊢ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) )
188	187	mptpreima	⊢ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = { 𝑤 ∈ 𝐵 ∣ ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 }
189	186 188	elrab2	⊢ ( 𝑝 ∈ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ↔ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) )
190	160 38	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
191	190	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
192		simprl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝑢 ∈ 𝐾 )
193	160 74	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐾 = ( MetOpen ‘ 𝐸 ) )
194	193	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝐾 = ( MetOpen ‘ 𝐸 ) )
195	192 194	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝑢 ∈ ( MetOpen ‘ 𝐸 ) )
196		simprrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 )
197	55	mopni2	⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑢 ∈ ( MetOpen ‘ 𝐸 ) ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) → ∃ 𝑟 ∈ ℝ⁺ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 )
198	191 195 196 197	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → ∃ 𝑟 ∈ ℝ⁺ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 )
199	21	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
200		simprrl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝑝 ∈ 𝐵 )
201	200	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑝 ∈ 𝐵 )
202		rpxr	⊢ ( 𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^* )
203	202	ad2antrl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑟 ∈ ℝ^* )
204	155	blopn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐷 ) )
205	199 201 203 204	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐷 ) )
206		simprl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑟 ∈ ℝ⁺ )
207		blcntr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺ ) → 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) )
208	199 201 206 207	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) )
209		blssm	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^* ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
210	199 201 203 209	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
211		simplrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 )
212		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝜑 )
213		rpgt0	⊢ ( 𝑟 ∈ ℝ⁺ → 0 < 𝑟 )
214	213	ad2antrl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 0 < 𝑟 )
215	212 201 203 214 96	syl121anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
216	215	eleq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ↔ 𝑤 ∈ X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
217	216	biimpa	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → 𝑤 ∈ X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
218		vex	⊢ 𝑤 ∈ V
219	218	elixp	⊢ ( 𝑤 ∈ X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ↔ ( 𝑤 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
220	219	simprbi	⊢ ( 𝑤 ∈ X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
221	217 220	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ∀ 𝑘 ∈ 𝐼 ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
222		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → 𝑘 ∈ 𝐼 )
223		rsp	⊢ ( ∀ 𝑘 ∈ 𝐼 ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( 𝑘 ∈ 𝐼 → ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
224	221 222 223	sylc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) )
225	211 224	sseldd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 )
226	210 225	ssrabdv	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ { 𝑤 ∈ 𝐵 ∣ ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 } )
227	226 188	sseqtrrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
228		eleq2	⊢ ( 𝑦 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑝 ∈ 𝑦 ↔ 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) )
229		sseq1	⊢ ( 𝑦 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ↔ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
230	228 229	anbi12d	⊢ ( 𝑦 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ↔ ( 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) )
231	230	rspcev	⊢ ( ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐷 ) ∧ ( 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
232	205 208 227 231	syl12anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
233	198 232	rexlimddv	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
234	233	expr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) )
235	189 234	biimtrid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑝 ∈ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) )
236	235	ralrimiv	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ∀ 𝑝 ∈ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
237	157	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( MetOpen ‘ 𝐷 ) ∈ Top )
238		eltop2	⊢ ( ( MetOpen ‘ 𝐷 ) ∈ Top → ( ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑝 ∈ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) )
239	237 238	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑝 ∈ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) )
240	236 239	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ^◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
241	184 240	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
242	241	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∀ 𝑢 ∈ 𝐾 ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
243	242 159	raleqtrrdv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
244	243	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
245		fveq2	⊢ ( 𝑘 = 𝑚 → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) )
246		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝑤 ‘ 𝑘 ) = ( 𝑤 ‘ 𝑚 ) )
247	246	mpteq2dv	⊢ ( 𝑘 = 𝑚 → ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) )
248	247	cnveqd	⊢ ( 𝑘 = 𝑚 → ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) )
249	248	imaeq1d	⊢ ( 𝑘 = 𝑚 → ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) )
250	249	eleq1d	⊢ ( 𝑘 = 𝑚 → ( ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) )
251	245 250	raleqbidv	⊢ ( 𝑘 = 𝑚 → ( ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) )
252	251	cbvralvw	⊢ ( ∀ 𝑘 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
253	244 252	sylib	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
254		eqid	⊢ ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) = ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) )
255	254	fmpox	⊢ ( ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) : ∪ 𝑚 ∈ 𝐼 ( { 𝑚 } × ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ) ⟶ ( MetOpen ‘ 𝐷 ) )
256	253 255	sylib	⊢ ( 𝜑 → ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) : ∪ 𝑚 ∈ 𝐼 ( { 𝑚 } × ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ) ⟶ ( MetOpen ‘ 𝐷 ) )
257	256	frnd	⊢ ( 𝜑 → ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ⊆ ( MetOpen ‘ 𝐷 ) )
258	180 257	unssd	⊢ ( 𝜑 → ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ⊆ ( MetOpen ‘ 𝐷 ) )
259		fiss	⊢ ( ( ( MetOpen ‘ 𝐷 ) ∈ Top ∧ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ⊆ ( MetOpen ‘ 𝐷 ) ) → ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) )
260	157 258 259	syl2anc	⊢ ( 𝜑 → ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ^◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) )
261	154 260	eqsstrd	⊢ ( 𝜑 → 𝐶 ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) )
262		fitop	⊢ ( ( MetOpen ‘ 𝐷 ) ∈ Top → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )
263	157 262	syl	⊢ ( 𝜑 → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )
264	155	mopnval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
265	21 264	syl	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
266		tgdif0	⊢ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) )
267	265 266	eqtr4di	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) )
268	263 267	eqtrd	⊢ ( 𝜑 → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) )
269	261 268	sseqtrd	⊢ ( 𝜑 → 𝐶 ⊆ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) )
270		2basgen	⊢ ( ( ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) ) → ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ 𝐶 ) )
271	137 269 270	syl2anc	⊢ ( 𝜑 → ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ 𝐶 ) )
272	19 271	eqtr4d	⊢ ( 𝜑 → ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) )
273	1 2 3 13 7	prdstopn	⊢ ( 𝜑 → 𝐽 = ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) )
274	272 273 267	3eqtr4d	⊢ ( 𝜑 → 𝐽 = ( MetOpen ‘ 𝐷 ) )

Metamath Proof Explorer

Theorem prdsxmslem2

Proof