Metamath Proof Explorer

Theorem hoiqssbl

Description: A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoiqssbl.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoiqssbl.y ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
hoiqssbl.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
Assertion hoiqssbl ( 𝜑 → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 hoiqssbl.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 hoiqssbl.y ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
3 hoiqssbl.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
4 0ex ⊢ ∅ ∈ V
5 4 snid ⊢ ∅ ∈ { ∅ }
6 5 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∅ ∈ { ∅ } )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
8 oveq2 ⊢ ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
9 reex ⊢ ℝ ∈ V
10 mapdm0 ⊢ ( ℝ ∈ V → ( ℝ ↑m ∅ ) = { ∅ } )
11 9 10 ax-mp ⊢ ( ℝ ↑m ∅ ) = { ∅ }
12 11 a1i ⊢ ( 𝑋 = ∅ → ( ℝ ↑m ∅ ) = { ∅ } )
13 8 12 eqtrd ⊢ ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) = { ∅ } )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ℝ ↑m 𝑋 ) = { ∅ } )
15 7 14 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝑌 ∈ { ∅ } )
16 0fi ⊢ ∅ ∈ Fin
17 eqid ⊢ ( dist ‘ ( ℝ^ ‘ ∅ ) ) = ( dist ‘ ( ℝ^ ‘ ∅ ) )
18 17 rrxmetfi ⊢ ( ∅ ∈ Fin → ( dist ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( Met ‘ ( ℝ ↑m ∅ ) ) )
19 16 18 ax-mp ⊢ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( Met ‘ ( ℝ ↑m ∅ ) )
20 metxmet ⊢ ( ( dist ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( Met ‘ ( ℝ ↑m ∅ ) ) → ( dist ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( ∞Met ‘ ( ℝ ↑m ∅ ) ) )
21 19 20 ax-mp ⊢ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( ∞Met ‘ ( ℝ ↑m ∅ ) )
22 21 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( dist ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( ∞Met ‘ ( ℝ ↑m ∅ ) ) )
23 6 11 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∅ ∈ ( ℝ ↑m ∅ ) )
24 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐸 ∈ ℝ+ )
25 blcntr ⊢ ( ( ( dist ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( ∞Met ‘ ( ℝ ↑m ∅ ) ) ∧ ∅ ∈ ( ℝ ↑m ∅ ) ∧ 𝐸 ∈ ℝ+ ) → ∅ ∈ ( ∅ ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) )
26 22 23 24 25 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∅ ∈ ( ∅ ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) )
27 elsni ⊢ ( 𝑌 ∈ { ∅ } → 𝑌 = ∅ )
28 15 27 syl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝑌 = ∅ )
29 28 eqcomd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∅ = 𝑌 )
30 29 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ∅ ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) = ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) )
31 26 30 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∅ ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) )
32 31 snssd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) )
33 15 32 jca ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) )
34 biidd ⊢ ( 𝑑 = ∅ → ( ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ↔ ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
35 34 rspcev ⊢ ( ( ∅ ∈ { ∅ } ∧ ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) → ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) )
36 6 33 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) )
37 biidd ⊢ ( 𝑐 = ∅ → ( ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ↔ ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
38 37 rspcev ⊢ ( ( ∅ ∈ { ∅ } ∧ ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) → ∃ 𝑐 ∈ { ∅ } ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) )
39 6 36 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∃ 𝑐 ∈ { ∅ } ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) )
40 oveq2 ⊢ ( 𝑋 = ∅ → ( ℚ ↑m 𝑋 ) = ( ℚ ↑m ∅ ) )
41 qex ⊢ ℚ ∈ V
42 mapdm0 ⊢ ( ℚ ∈ V → ( ℚ ↑m ∅ ) = { ∅ } )
43 41 42 ax-mp ⊢ ( ℚ ↑m ∅ ) = { ∅ }
44 43 a1i ⊢ ( 𝑋 = ∅ → ( ℚ ↑m ∅ ) = { ∅ } )
45 40 44 eqtr2d ⊢ ( 𝑋 = ∅ → { ∅ } = ( ℚ ↑m 𝑋 ) )
46 45 eqcomd ⊢ ( 𝑋 = ∅ → ( ℚ ↑m 𝑋 ) = { ∅ } )
47 46 eleq2d ⊢ ( 𝑋 = ∅ → ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ↔ 𝑐 ∈ { ∅ } ) )
48 46 eleq2d ⊢ ( 𝑋 = ∅ → ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ↔ 𝑑 ∈ { ∅ } ) )
49 48 anbi1d ⊢ ( 𝑋 = ∅ → ( ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∧ ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) ↔ ( 𝑑 ∈ { ∅ } ∧ ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) ) )
50 49 rexbidv2 ⊢ ( 𝑋 = ∅ → ( ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ↔ ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
51 47 50 anbi12d ⊢ ( 𝑋 = ∅ → ( ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∧ ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) ↔ ( 𝑐 ∈ { ∅ } ∧ ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) ) )
52 51 rexbidv2 ⊢ ( 𝑋 = ∅ → ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ↔ ∃ 𝑐 ∈ { ∅ } ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ↔ ∃ 𝑐 ∈ { ∅ } ∃ 𝑑 ∈ { ∅ } ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
54 39 53 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) )
55 ixpeq1 ⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) = X 𝑖 ∈ ∅ ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) )
56 ixp0x ⊢ X 𝑖 ∈ ∅ ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) = { ∅ }
57 56 a1i ⊢ ( 𝑋 = ∅ → X 𝑖 ∈ ∅ ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) = { ∅ } )
58 55 57 eqtrd ⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) = { ∅ } )
59 58 eleq2d ⊢ ( 𝑋 = ∅ → ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ↔ 𝑌 ∈ { ∅ } ) )
60 2fveq3 ⊢ ( 𝑋 = ∅ → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( dist ‘ ( ℝ^ ‘ ∅ ) ) )
61 60 fveq2d ⊢ ( 𝑋 = ∅ → ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) = ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) )
62 61 oveqd ⊢ ( 𝑋 = ∅ → ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) = ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) )
63 58 62 sseq12d ⊢ ( 𝑋 = ∅ → ( X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ↔ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) )
64 59 63 anbi12d ⊢ ( 𝑋 = ∅ → ( ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) ↔ ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
65 64 rexbidv ⊢ ( 𝑋 = ∅ → ( ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) ↔ ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
66 65 rexbidv ⊢ ( 𝑋 = ∅ → ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) ↔ ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) ↔ ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ { ∅ } ∧ { ∅ } ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ ∅ ) ) ) 𝐸 ) ) ) )
68 54 67 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) )
69 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ∈ Fin )
70 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
71 70 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
72 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
73 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐸 ∈ ℝ+ )
74 69 71 72 73 hoiqssbllem3 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) )
75 68 74 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) )