# Metamath Proof Explorer

## Theorem ssbnd

Description: A subset of a metric space is bounded iff it is contained in a ball around P , for any P in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypothesis ssbnd.2 ${⊢}{N}={{M}↾}_{\left({Y}×{Y}\right)}$
Assertion ssbnd ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\to \left({N}\in \mathrm{Bnd}\left({Y}\right)↔\exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$

### Proof

Step Hyp Ref Expression
1 ssbnd.2 ${⊢}{N}={{M}↾}_{\left({Y}×{Y}\right)}$
2 0re ${⊢}0\in ℝ$
3 2 ne0ii ${⊢}ℝ\ne \varnothing$
4 0ss ${⊢}\varnothing \subseteq {P}\mathrm{ball}\left({M}\right){d}$
5 sseq1 ${⊢}{Y}=\varnothing \to \left({Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}↔\varnothing \subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
6 4 5 mpbiri ${⊢}{Y}=\varnothing \to {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}$
7 6 ralrimivw ${⊢}{Y}=\varnothing \to \forall {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}$
8 r19.2z ${⊢}\left(ℝ\ne \varnothing \wedge \forall {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}$
9 3 7 8 sylancr ${⊢}{Y}=\varnothing \to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}$
10 9 a1i ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{Bnd}\left({Y}\right)\right)\to \left({Y}=\varnothing \to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
11 isbnd2 ${⊢}\left({N}\in \mathrm{Bnd}\left({Y}\right)\wedge {Y}\ne \varnothing \right)↔\left({N}\in \mathrm{\infty Met}\left({Y}\right)\wedge \exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}={y}\mathrm{ball}\left({N}\right){r}\right)$
12 simplll ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {M}\in \mathrm{Met}\left({X}\right)$
13 1 dmeqi ${⊢}\mathrm{dom}{N}=\mathrm{dom}\left({{M}↾}_{\left({Y}×{Y}\right)}\right)$
14 dmres ${⊢}\mathrm{dom}\left({{M}↾}_{\left({Y}×{Y}\right)}\right)=\left({Y}×{Y}\right)\cap \mathrm{dom}{M}$
15 13 14 eqtri ${⊢}\mathrm{dom}{N}=\left({Y}×{Y}\right)\cap \mathrm{dom}{M}$
16 xmetf ${⊢}{N}\in \mathrm{\infty Met}\left({Y}\right)\to {N}:{Y}×{Y}⟶{ℝ}^{*}$
17 16 fdmd ${⊢}{N}\in \mathrm{\infty Met}\left({Y}\right)\to \mathrm{dom}{N}={Y}×{Y}$
18 15 17 syl5eqr ${⊢}{N}\in \mathrm{\infty Met}\left({Y}\right)\to \left({Y}×{Y}\right)\cap \mathrm{dom}{M}={Y}×{Y}$
19 df-ss ${⊢}{Y}×{Y}\subseteq \mathrm{dom}{M}↔\left({Y}×{Y}\right)\cap \mathrm{dom}{M}={Y}×{Y}$
20 18 19 sylibr ${⊢}{N}\in \mathrm{\infty Met}\left({Y}\right)\to {Y}×{Y}\subseteq \mathrm{dom}{M}$
21 20 ad2antlr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {Y}×{Y}\subseteq \mathrm{dom}{M}$
22 metf ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}:{X}×{X}⟶ℝ$
23 22 fdmd ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \mathrm{dom}{M}={X}×{X}$
24 23 ad3antrrr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to \mathrm{dom}{M}={X}×{X}$
25 21 24 sseqtrd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {Y}×{Y}\subseteq {X}×{X}$
26 dmss ${⊢}{Y}×{Y}\subseteq {X}×{X}\to \mathrm{dom}\left({Y}×{Y}\right)\subseteq \mathrm{dom}\left({X}×{X}\right)$
27 25 26 syl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to \mathrm{dom}\left({Y}×{Y}\right)\subseteq \mathrm{dom}\left({X}×{X}\right)$
28 dmxpid ${⊢}\mathrm{dom}\left({Y}×{Y}\right)={Y}$
29 dmxpid ${⊢}\mathrm{dom}\left({X}×{X}\right)={X}$
30 27 28 29 3sstr3g ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {Y}\subseteq {X}$
31 simprl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\in {Y}$
32 30 31 sseldd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\in {X}$
33 simpllr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {P}\in {X}$
34 metcl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\wedge {P}\in {X}\right)\to {y}{M}{P}\in ℝ$
35 12 32 33 34 syl3anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}{M}{P}\in ℝ$
36 rpre ${⊢}{r}\in {ℝ}^{+}\to {r}\in ℝ$
37 36 ad2antll ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {r}\in ℝ$
38 35 37 readdcld ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to \left({y}{M}{P}\right)+{r}\in ℝ$
39 metxmet ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
40 12 39 syl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
41 32 31 elind ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\in \left({X}\cap {Y}\right)$
42 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
43 42 ad2antll ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {r}\in {ℝ}^{*}$
44 1 blres ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in \left({X}\cap {Y}\right)\wedge {r}\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({N}\right){r}=\left({y}\mathrm{ball}\left({M}\right){r}\right)\cap {Y}$
45 40 41 43 44 syl3anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\mathrm{ball}\left({N}\right){r}=\left({y}\mathrm{ball}\left({M}\right){r}\right)\cap {Y}$
46 inss1 ${⊢}\left({y}\mathrm{ball}\left({M}\right){r}\right)\cap {Y}\subseteq {y}\mathrm{ball}\left({M}\right){r}$
47 35 leidd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}{M}{P}\le {y}{M}{P}$
48 35 recnd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}{M}{P}\in ℂ$
49 37 recnd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {r}\in ℂ$
50 48 49 pncand ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to \left({y}{M}{P}\right)+{r}-{r}={y}{M}{P}$
51 47 50 breqtrrd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}{M}{P}\le \left({y}{M}{P}\right)+{r}-{r}$
52 blss2 ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {P}\in {X}\right)\wedge \left({r}\in ℝ\wedge \left({y}{M}{P}\right)+{r}\in ℝ\wedge {y}{M}{P}\le \left({y}{M}{P}\right)+{r}-{r}\right)\right)\to {y}\mathrm{ball}\left({M}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right)\left(\left({y}{M}{P}\right)+{r}\right)$
53 40 32 33 37 38 51 52 syl33anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\mathrm{ball}\left({M}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right)\left(\left({y}{M}{P}\right)+{r}\right)$
54 46 53 sstrid ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to \left({y}\mathrm{ball}\left({M}\right){r}\right)\cap {Y}\subseteq {P}\mathrm{ball}\left({M}\right)\left(\left({y}{M}{P}\right)+{r}\right)$
55 45 54 eqsstrd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to {y}\mathrm{ball}\left({N}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right)\left(\left({y}{M}{P}\right)+{r}\right)$
56 oveq2 ${⊢}{d}=\left({y}{M}{P}\right)+{r}\to {P}\mathrm{ball}\left({M}\right){d}={P}\mathrm{ball}\left({M}\right)\left(\left({y}{M}{P}\right)+{r}\right)$
57 56 sseq2d ${⊢}{d}=\left({y}{M}{P}\right)+{r}\to \left({y}\mathrm{ball}\left({N}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right){d}↔{y}\mathrm{ball}\left({N}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right)\left(\left({y}{M}{P}\right)+{r}\right)\right)$
58 57 rspcev ${⊢}\left(\left({y}{M}{P}\right)+{r}\in ℝ\wedge {y}\mathrm{ball}\left({N}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right)\left(\left({y}{M}{P}\right)+{r}\right)\right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({N}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right){d}$
59 38 55 58 syl2anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({N}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right){d}$
60 sseq1 ${⊢}{Y}={y}\mathrm{ball}\left({N}\right){r}\to \left({Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}↔{y}\mathrm{ball}\left({N}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
61 60 rexbidv ${⊢}{Y}={y}\mathrm{ball}\left({N}\right){r}\to \left(\exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}↔\exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({N}\right){r}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
62 59 61 syl5ibrcom ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\wedge \left({y}\in {Y}\wedge {r}\in {ℝ}^{+}\right)\right)\to \left({Y}={y}\mathrm{ball}\left({N}\right){r}\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
63 62 rexlimdvva ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{\infty Met}\left({Y}\right)\right)\to \left(\exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}={y}\mathrm{ball}\left({N}\right){r}\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
64 63 expimpd ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\to \left(\left({N}\in \mathrm{\infty Met}\left({Y}\right)\wedge \exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}={y}\mathrm{ball}\left({N}\right){r}\right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
65 11 64 syl5bi ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\to \left(\left({N}\in \mathrm{Bnd}\left({Y}\right)\wedge {Y}\ne \varnothing \right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
66 65 expdimp ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{Bnd}\left({Y}\right)\right)\to \left({Y}\ne \varnothing \to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
67 10 66 pm2.61dne ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {N}\in \mathrm{Bnd}\left({Y}\right)\right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}$
68 67 ex ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\to \left({N}\in \mathrm{Bnd}\left({Y}\right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$
69 simprr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge \left({d}\in ℝ\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\right)\to {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}$
70 xpss12 ${⊢}\left({Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\to {Y}×{Y}\subseteq \left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)$
71 69 69 70 syl2anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge \left({d}\in ℝ\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\right)\to {Y}×{Y}\subseteq \left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)$
72 71 resabs1d ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge \left({d}\in ℝ\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\right)\to {\left({{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\right)↾}_{\left({Y}×{Y}\right)}={{M}↾}_{\left({Y}×{Y}\right)}$
73 72 1 syl6eqr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge \left({d}\in ℝ\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\right)\to {\left({{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\right)↾}_{\left({Y}×{Y}\right)}={N}$
74 blbnd ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {d}\in ℝ\right)\to {{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\in \mathrm{Bnd}\left({P}\mathrm{ball}\left({M}\right){d}\right)$
75 39 74 syl3an1 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\wedge {d}\in ℝ\right)\to {{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\in \mathrm{Bnd}\left({P}\mathrm{ball}\left({M}\right){d}\right)$
76 75 3expa ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {d}\in ℝ\right)\to {{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\in \mathrm{Bnd}\left({P}\mathrm{ball}\left({M}\right){d}\right)$
77 76 adantrr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge \left({d}\in ℝ\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\right)\to {{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\in \mathrm{Bnd}\left({P}\mathrm{ball}\left({M}\right){d}\right)$
78 bndss ${⊢}\left({{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\in \mathrm{Bnd}\left({P}\mathrm{ball}\left({M}\right){d}\right)\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\to {\left({{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\right)↾}_{\left({Y}×{Y}\right)}\in \mathrm{Bnd}\left({Y}\right)$
79 77 69 78 syl2anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge \left({d}\in ℝ\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\right)\to {\left({{M}↾}_{\left(\left({P}\mathrm{ball}\left({M}\right){d}\right)×\left({P}\mathrm{ball}\left({M}\right){d}\right)\right)}\right)↾}_{\left({Y}×{Y}\right)}\in \mathrm{Bnd}\left({Y}\right)$
80 73 79 eqeltrrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge \left({d}\in ℝ\wedge {Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)\right)\to {N}\in \mathrm{Bnd}\left({Y}\right)$
81 80 rexlimdvaa ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\to \left(\exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\to {N}\in \mathrm{Bnd}\left({Y}\right)\right)$
82 68 81 impbid ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {P}\in {X}\right)\to \left({N}\in \mathrm{Bnd}\left({Y}\right)↔\exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{Y}\subseteq {P}\mathrm{ball}\left({M}\right){d}\right)$