This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blss

Description: Any point P in a ball B can be centered in another ball that is a subset of B . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion blss ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝐵 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 blrn ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) ↔ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ* 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
2 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑃 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑃 ) < 𝑟 ) ) )
3 simpl1 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 simpl2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
5 simpr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
6 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑦 𝐷 𝑃 ) ∈ ℝ* )
7 3 4 5 6 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑦 𝐷 𝑃 ) ∈ ℝ* )
8 simpl3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → 𝑟 ∈ ℝ* )
9 qbtwnxr ⊢ ( ( ( 𝑦 𝐷 𝑃 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ∧ ( 𝑦 𝐷 𝑃 ) < 𝑟 ) → ∃ 𝑧 ∈ ℚ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) )
10 9 3expia ⊢ ( ( ( 𝑦 𝐷 𝑃 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑦 𝐷 𝑃 ) < 𝑟 → ∃ 𝑧 ∈ ℚ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) )
11 7 8 10 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑦 𝐷 𝑃 ) < 𝑟 → ∃ 𝑧 ∈ ℚ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) )
12 qre ⊢ ( 𝑧 ∈ ℚ → 𝑧 ∈ ℝ )
13 simpll1 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
14 simplr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑃 ∈ 𝑋 )
15 simpll2 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑦 ∈ 𝑋 )
16 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑃 ) )
17 13 14 15 16 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑃 ) )
18 simprrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑦 𝐷 𝑃 ) < 𝑧 )
19 17 18 eqbrtrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) < 𝑧 )
20 simprl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 ∈ ℝ )
21 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ* )
22 13 14 15 21 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ* )
23 rexr ⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℝ* )
24 23 ad2antrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 ∈ ℝ* )
25 22 24 19 xrltled ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ≤ 𝑧 )
26 xmetlecl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑃 𝐷 𝑦 ) ≤ 𝑧 ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ )
27 13 14 15 20 25 26 syl122anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℝ )
28 difrp ⊢ ( ( ( 𝑃 𝐷 𝑦 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑃 𝐷 𝑦 ) < 𝑧 ↔ ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ+ ) )
29 27 20 28 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( ( 𝑃 𝐷 𝑦 ) < 𝑧 ↔ ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ+ ) )
30 19 29 mpbid ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ+ )
31 20 27 resubcld ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ )
32 22 xrleidd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ≤ ( 𝑃 𝐷 𝑦 ) )
33 20 recnd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 ∈ ℂ )
34 27 recnd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ∈ ℂ )
35 33 34 nncand ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑧 − ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) = ( 𝑃 𝐷 𝑦 ) )
36 32 35 breqtrrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 𝐷 𝑦 ) ≤ ( 𝑧 − ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) )
37 blss2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ ( 𝑃 𝐷 𝑦 ) ≤ ( 𝑧 − ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑧 ) )
38 13 14 15 31 20 36 37 syl33anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑧 ) )
39 simpll3 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑟 ∈ ℝ* )
40 simprrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 < 𝑟 )
41 24 39 40 xrltled ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → 𝑧 ≤ 𝑟 )
42 ssbl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) ∧ 𝑧 ≤ 𝑟 ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
43 13 15 24 39 41 42 syl221anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑧 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
44 38 43 sstrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
45 oveq2 ⊢ ( 𝑥 = ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) = ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) )
46 45 sseq1d ⊢ ( 𝑥 = ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
47 46 rspcev ⊢ ( ( ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ 𝐷 ) ( 𝑧 − ( 𝑃 𝐷 𝑦 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
48 30 44 47 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
49 48 expr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
50 12 49 sylan2 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑧 ∈ ℚ ) → ( ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
51 50 rexlimdva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ ℚ ( ( 𝑦 𝐷 𝑃 ) < 𝑧 ∧ 𝑧 < 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
52 11 51 syld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑦 𝐷 𝑃 ) < 𝑟 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
53 52 expimpd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑃 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑃 ) < 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
54 2 53 sylbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑃 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
55 eleq2 ⊢ ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝐵 ↔ 𝑃 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
56 sseq2 ⊢ ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ↔ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
57 56 rexbidv ⊢ ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ↔ ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
58 55 57 imbi12d ⊢ ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ↔ ( 𝑃 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
59 54 58 syl5ibrcom ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ) )
60 59 3expib ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ) ) )
61 60 rexlimdvv ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ* 𝐵 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ) )
62 1 61 sylbid ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐵 ∈ ran ( ball ‘ 𝐷 ) → ( 𝑃 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 ) ) )
63 62 3imp ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑃 ∈ 𝐵 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐵 )