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 ‘ 𝐷 ) )