# 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 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {B}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\wedge {P}\in {B}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {B}$

### Proof

Step Hyp Ref Expression
1 blrn ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({B}\in \mathrm{ran}\mathrm{ball}\left({D}\right)↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{B}={y}\mathrm{ball}\left({D}\right){r}\right)$
2 elbl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to \left({P}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)↔\left({P}\in {X}\wedge {y}{D}{P}<{r}\right)\right)$
3 simpl1 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
4 simpl2 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\to {y}\in {X}$
5 simpr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\to {P}\in {X}$
6 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {P}\in {X}\right)\to {y}{D}{P}\in {ℝ}^{*}$
7 3 4 5 6 syl3anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\to {y}{D}{P}\in {ℝ}^{*}$
8 simpl3 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\to {r}\in {ℝ}^{*}$
9 qbtwnxr ${⊢}\left({y}{D}{P}\in {ℝ}^{*}\wedge {r}\in {ℝ}^{*}\wedge {y}{D}{P}<{r}\right)\to \exists {z}\in ℚ\phantom{\rule{.4em}{0ex}}\left({y}{D}{P}<{z}\wedge {z}<{r}\right)$
10 9 3expia ${⊢}\left({y}{D}{P}\in {ℝ}^{*}\wedge {r}\in {ℝ}^{*}\right)\to \left({y}{D}{P}<{r}\to \exists {z}\in ℚ\phantom{\rule{.4em}{0ex}}\left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)$
11 7 8 10 syl2anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\to \left({y}{D}{P}<{r}\to \exists {z}\in ℚ\phantom{\rule{.4em}{0ex}}\left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)$
12 qre ${⊢}{z}\in ℚ\to {z}\in ℝ$
13 simpll1 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
14 simplr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}\in {X}$
15 simpll2 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {y}\in {X}$
16 xmetsym ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {y}\in {X}\right)\to {P}{D}{y}={y}{D}{P}$
17 13 14 15 16 syl3anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}{D}{y}={y}{D}{P}$
18 simprrl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {y}{D}{P}<{z}$
19 17 18 eqbrtrd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}{D}{y}<{z}$
20 simprl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {z}\in ℝ$
21 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {y}\in {X}\right)\to {P}{D}{y}\in {ℝ}^{*}$
22 13 14 15 21 syl3anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}{D}{y}\in {ℝ}^{*}$
23 rexr ${⊢}{z}\in ℝ\to {z}\in {ℝ}^{*}$
24 23 ad2antrl ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {z}\in {ℝ}^{*}$
25 22 24 19 xrltled ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}{D}{y}\le {z}$
26 xmetlecl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({P}\in {X}\wedge {y}\in {X}\right)\wedge \left({z}\in ℝ\wedge {P}{D}{y}\le {z}\right)\right)\to {P}{D}{y}\in ℝ$
27 13 14 15 20 25 26 syl122anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}{D}{y}\in ℝ$
28 difrp ${⊢}\left({P}{D}{y}\in ℝ\wedge {z}\in ℝ\right)\to \left({P}{D}{y}<{z}↔{z}-\left({P}{D}{y}\right)\in {ℝ}^{+}\right)$
29 27 20 28 syl2anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to \left({P}{D}{y}<{z}↔{z}-\left({P}{D}{y}\right)\in {ℝ}^{+}\right)$
30 19 29 mpbid ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {z}-\left({P}{D}{y}\right)\in {ℝ}^{+}$
31 20 27 resubcld ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {z}-\left({P}{D}{y}\right)\in ℝ$
32 22 xrleidd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}{D}{y}\le {P}{D}{y}$
33 20 recnd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {z}\in ℂ$
34 27 recnd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}{D}{y}\in ℂ$
35 33 34 nncand ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {z}-\left({z}-\left({P}{D}{y}\right)\right)={P}{D}{y}$
36 32 35 breqtrrd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}{D}{y}\le {z}-\left({z}-\left({P}{D}{y}\right)\right)$
37 blss2 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {y}\in {X}\right)\wedge \left({z}-\left({P}{D}{y}\right)\in ℝ\wedge {z}\in ℝ\wedge {P}{D}{y}\le {z}-\left({z}-\left({P}{D}{y}\right)\right)\right)\right)\to {P}\mathrm{ball}\left({D}\right)\left({z}-\left({P}{D}{y}\right)\right)\subseteq {y}\mathrm{ball}\left({D}\right){z}$
38 13 14 15 31 20 36 37 syl33anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}\mathrm{ball}\left({D}\right)\left({z}-\left({P}{D}{y}\right)\right)\subseteq {y}\mathrm{ball}\left({D}\right){z}$
39 simpll3 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {r}\in {ℝ}^{*}$
40 simprrr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {z}<{r}$
41 24 39 40 xrltled ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {z}\le {r}$
42 ssbl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({z}\in {ℝ}^{*}\wedge {r}\in {ℝ}^{*}\right)\wedge {z}\le {r}\right)\to {y}\mathrm{ball}\left({D}\right){z}\subseteq {y}\mathrm{ball}\left({D}\right){r}$
43 13 15 24 39 41 42 syl221anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {y}\mathrm{ball}\left({D}\right){z}\subseteq {y}\mathrm{ball}\left({D}\right){r}$
44 38 43 sstrd ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to {P}\mathrm{ball}\left({D}\right)\left({z}-\left({P}{D}{y}\right)\right)\subseteq {y}\mathrm{ball}\left({D}\right){r}$
45 oveq2 ${⊢}{x}={z}-\left({P}{D}{y}\right)\to {P}\mathrm{ball}\left({D}\right){x}={P}\mathrm{ball}\left({D}\right)\left({z}-\left({P}{D}{y}\right)\right)$
46 45 sseq1d ${⊢}{x}={z}-\left({P}{D}{y}\right)\to \left({P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}↔{P}\mathrm{ball}\left({D}\right)\left({z}-\left({P}{D}{y}\right)\right)\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
47 46 rspcev ${⊢}\left({z}-\left({P}{D}{y}\right)\in {ℝ}^{+}\wedge {P}\mathrm{ball}\left({D}\right)\left({z}-\left({P}{D}{y}\right)\right)\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}$
48 30 44 47 syl2anc ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge \left({z}\in ℝ\wedge \left({y}{D}{P}<{z}\wedge {z}<{r}\right)\right)\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}$
49 48 expr ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge {z}\in ℝ\right)\to \left(\left({y}{D}{P}<{z}\wedge {z}<{r}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
50 12 49 sylan2 ${⊢}\left(\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\wedge {z}\in ℚ\right)\to \left(\left({y}{D}{P}<{z}\wedge {z}<{r}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
51 50 rexlimdva ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\to \left(\exists {z}\in ℚ\phantom{\rule{.4em}{0ex}}\left({y}{D}{P}<{z}\wedge {z}<{r}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
52 11 51 syld ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\wedge {P}\in {X}\right)\to \left({y}{D}{P}<{r}\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
53 52 expimpd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to \left(\left({P}\in {X}\wedge {y}{D}{P}<{r}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
54 2 53 sylbid ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to \left({P}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
55 eleq2 ${⊢}{B}={y}\mathrm{ball}\left({D}\right){r}\to \left({P}\in {B}↔{P}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\right)$
56 sseq2 ${⊢}{B}={y}\mathrm{ball}\left({D}\right){r}\to \left({P}\mathrm{ball}\left({D}\right){x}\subseteq {B}↔{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
57 56 rexbidv ${⊢}{B}={y}\mathrm{ball}\left({D}\right){r}\to \left(\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {B}↔\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)$
58 55 57 imbi12d ${⊢}{B}={y}\mathrm{ball}\left({D}\right){r}\to \left(\left({P}\in {B}\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {B}\right)↔\left({P}\in \left({y}\mathrm{ball}\left({D}\right){r}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {y}\mathrm{ball}\left({D}\right){r}\right)\right)$
59 54 58 syl5ibrcom ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to \left({B}={y}\mathrm{ball}\left({D}\right){r}\to \left({P}\in {B}\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {B}\right)\right)$
60 59 3expib ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to \left({B}={y}\mathrm{ball}\left({D}\right){r}\to \left({P}\in {B}\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {B}\right)\right)\right)$
61 60 rexlimdvv ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{B}={y}\mathrm{ball}\left({D}\right){r}\to \left({P}\in {B}\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {B}\right)\right)$
62 1 61 sylbid ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({B}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\to \left({P}\in {B}\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {B}\right)\right)$
63 62 3imp ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {B}\in \mathrm{ran}\mathrm{ball}\left({D}\right)\wedge {P}\in {B}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{P}\mathrm{ball}\left({D}\right){x}\subseteq {B}$