Metamath Proof Explorer

Theorem 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 ⊢ 𝑌 = ( 𝑆 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 prdsxmslem2 ( 𝜑 → 𝐽 = ( MetOpen ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 prdsxms.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp )
38 8 9 xmsxmet ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
39 37 38 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
40 eqid ⊢ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
41 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
42 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑆 ∈ 𝑊 )
43 37 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp )
44 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ 𝐵 )
45 36 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑅 = ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
46 45 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
47 1 46 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑌 = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
48 47 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
49 5 48 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
50 44 49 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
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 < 𝑟 ) → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) )
81 1 80 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑌 = ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) )
82 81 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
83 4 82 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
84 83 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( ball ‘ 𝐷 ) = ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) )
85 84 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑝 ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) )
86 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑅 ‘ 𝑛 ) = ( 𝑅 ‘ 𝑘 ) )
87 86 cbvmptv ⊢ ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) )
88 87 oveq2i ⊢ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
89 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) )
90 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) )
91 81 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
92 5 91 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
93 44 92 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) )
94 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 0 < 𝑟 )
95 88 89 8 9 90 42 29 37 39 93 53 94 prdsbl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑝 ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) = 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 syl5bi ⊢ ( 𝜑 → ( 𝑥 ∈ ( 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ ∞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 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑝 ∈ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ∃ 𝑦 ∈ ( 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 159 raleqdv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑢 ∈ 𝐾 ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) )
244 242 243 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
245 244 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
246 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) )
247 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑤 ‘ 𝑘 ) = ( 𝑤 ‘ 𝑚 ) )
248 247 mpteq2dv ⊢ ( 𝑘 = 𝑚 → ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) )
249 248 cnveqd ⊢ ( 𝑘 = 𝑚 → ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) )
250 249 imaeq1d ⊢ ( 𝑘 = 𝑚 → ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) )
251 250 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) )
252 246 251 raleqbidv ⊢ ( 𝑘 = 𝑚 → ( ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) )
253 252 cbvralvw ⊢ ( ∀ 𝑘 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
254 245 253 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) )
255 eqid ⊢ ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) = ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) )
256 255 fmpox ⊢ ( ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) : ∪ 𝑚 ∈ 𝐼 ( { 𝑚 } × ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ) ⟶ ( MetOpen ‘ 𝐷 ) )
257 254 256 sylib ⊢ ( 𝜑 → ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) : ∪ 𝑚 ∈ 𝐼 ( { 𝑚 } × ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ) ⟶ ( MetOpen ‘ 𝐷 ) )
258 257 frnd ⊢ ( 𝜑 → ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ⊆ ( MetOpen ‘ 𝐷 ) )
259 180 258 unssd ⊢ ( 𝜑 → ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ⊆ ( MetOpen ‘ 𝐷 ) )
260 fiss ⊢ ( ( ( MetOpen ‘ 𝐷 ) ∈ Top ∧ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ⊆ ( MetOpen ‘ 𝐷 ) ) → ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) )
261 157 259 260 syl2anc ⊢ ( 𝜑 → ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) )
262 154 261 eqsstrd ⊢ ( 𝜑 → 𝐶 ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) )
263 fitop ⊢ ( ( MetOpen ‘ 𝐷 ) ∈ Top → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )
264 157 263 syl ⊢ ( 𝜑 → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )
265 155 mopnval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
266 21 265 syl ⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
267 tgdif0 ⊢ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) )
268 266 267 eqtr4di ⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) )
269 264 268 eqtrd ⊢ ( 𝜑 → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) )
270 262 269 sseqtrd ⊢ ( 𝜑 → 𝐶 ⊆ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) )
271 2basgen ⊢ ( ( ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) ) → ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ 𝐶 ) )
272 137 270 271 syl2anc ⊢ ( 𝜑 → ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ 𝐶 ) )
273 19 272 eqtr4d ⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) )
274 1 2 3 13 7 prdstopn ⊢ ( 𝜑 → 𝐽 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
275 273 274 268 3eqtr4d ⊢ ( 𝜑 → 𝐽 = ( MetOpen ‘ 𝐷 ) )