# Metamath Proof Explorer

## Theorem blbnd

Description: A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 15-Jan-2014)

Ref Expression
Assertion blbnd ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\to {{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{Bnd}\left({Y}\mathrm{ball}\left({M}\right){R}\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
2 rexr ${⊢}{R}\in ℝ\to {R}\in {ℝ}^{*}$
3 blssm ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to {Y}\mathrm{ball}\left({M}\right){R}\subseteq {X}$
4 2 3 syl3an3 ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\to {Y}\mathrm{ball}\left({M}\right){R}\subseteq {X}$
5 xmetres2 ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\subseteq {X}\right)\to {{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{\infty Met}\left({Y}\mathrm{ball}\left({M}\right){R}\right)$
6 1 4 5 syl2anc ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\to {{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{\infty Met}\left({Y}\mathrm{ball}\left({M}\right){R}\right)$
7 6 adantr ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}=\varnothing \right)\to {{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{\infty Met}\left({Y}\mathrm{ball}\left({M}\right){R}\right)$
8 rzal ${⊢}{Y}\mathrm{ball}\left({M}\right){R}=\varnothing \to \forall {x}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}\mathrm{ball}\left({M}\right){R}={x}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){r}$
9 8 adantl ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}=\varnothing \right)\to \forall {x}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}\mathrm{ball}\left({M}\right){R}={x}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){r}$
10 isbndx ${⊢}{{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{Bnd}\left({Y}\mathrm{ball}\left({M}\right){R}\right)↔\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{\infty Met}\left({Y}\mathrm{ball}\left({M}\right){R}\right)\wedge \forall {x}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}\mathrm{ball}\left({M}\right){R}={x}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){r}\right)$
11 7 9 10 sylanbrc ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}=\varnothing \right)\to {{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{Bnd}\left({Y}\mathrm{ball}\left({M}\right){R}\right)$
12 6 adantr ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{\infty Met}\left({Y}\mathrm{ball}\left({M}\right){R}\right)$
13 1 adantr ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
14 simpl2 ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {Y}\in {X}$
15 simpl3 ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {R}\in ℝ$
16 xbln0 ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to \left({Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing ↔0<{R}\right)$
17 2 16 syl3an3 ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\to \left({Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing ↔0<{R}\right)$
18 17 biimpa ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to 0<{R}$
19 15 18 elrpd ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {R}\in {ℝ}^{+}$
20 blcntr ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in {ℝ}^{+}\right)\to {Y}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)$
21 13 14 19 20 syl3anc ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {Y}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)$
22 14 21 elind ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {Y}\in \left({X}\cap \left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)$
23 15 rexrd ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {R}\in {ℝ}^{*}$
24 eqid ${⊢}{{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}={{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}$
25 24 blres ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in \left({X}\cap \left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)\wedge {R}\in {ℝ}^{*}\right)\to {Y}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){R}=\left({Y}\mathrm{ball}\left({M}\right){R}\right)\cap \left({Y}\mathrm{ball}\left({M}\right){R}\right)$
26 13 22 23 25 syl3anc ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {Y}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){R}=\left({Y}\mathrm{ball}\left({M}\right){R}\right)\cap \left({Y}\mathrm{ball}\left({M}\right){R}\right)$
27 inidm ${⊢}\left({Y}\mathrm{ball}\left({M}\right){R}\right)\cap \left({Y}\mathrm{ball}\left({M}\right){R}\right)={Y}\mathrm{ball}\left({M}\right){R}$
28 26 27 syl6req ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {Y}\mathrm{ball}\left({M}\right){R}={Y}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){R}$
29 rspceov ${⊢}\left({Y}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)\wedge {R}\in {ℝ}^{+}\wedge {Y}\mathrm{ball}\left({M}\right){R}={Y}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){R}\right)\to \exists {x}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}\mathrm{ball}\left({M}\right){R}={x}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){r}$
30 21 19 28 29 syl3anc ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to \exists {x}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}\mathrm{ball}\left({M}\right){R}={x}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){r}$
31 isbnd2 ${⊢}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{Bnd}\left({Y}\mathrm{ball}\left({M}\right){R}\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)↔\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{\infty Met}\left({Y}\mathrm{ball}\left({M}\right){R}\right)\wedge \exists {x}\in \left({Y}\mathrm{ball}\left({M}\right){R}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{Y}\mathrm{ball}\left({M}\right){R}={x}\mathrm{ball}\left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\right){r}\right)$
32 12 30 31 sylanbrc ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to \left({{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{Bnd}\left({Y}\mathrm{ball}\left({M}\right){R}\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)$
33 32 simpld ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\wedge {Y}\mathrm{ball}\left({M}\right){R}\ne \varnothing \right)\to {{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{Bnd}\left({Y}\mathrm{ball}\left({M}\right){R}\right)$
34 11 33 pm2.61dane ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\in {X}\wedge {R}\in ℝ\right)\to {{M}↾}_{\left(\left({Y}\mathrm{ball}\left({M}\right){R}\right)×\left({Y}\mathrm{ball}\left({M}\right){R}\right)\right)}\in \mathrm{Bnd}\left({Y}\mathrm{ball}\left({M}\right){R}\right)$