# Metamath Proof Explorer

## Theorem bndss

Description: A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion bndss ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {S}\subseteq {X}\right)\to {{M}↾}_{\left({S}×{S}\right)}\in \mathrm{Bnd}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 metres2 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\to {{M}↾}_{\left({S}×{S}\right)}\in \mathrm{Met}\left({S}\right)$
2 1 adantlr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\wedge {S}\subseteq {X}\right)\to {{M}↾}_{\left({S}×{S}\right)}\in \mathrm{Met}\left({S}\right)$
3 ssel2 ${⊢}\left({S}\subseteq {X}\wedge {x}\in {S}\right)\to {x}\in {X}$
4 3 ancoms ${⊢}\left({x}\in {S}\wedge {S}\subseteq {X}\right)\to {x}\in {X}$
5 oveq1 ${⊢}{y}={x}\to {y}\mathrm{ball}\left({M}\right){r}={x}\mathrm{ball}\left({M}\right){r}$
6 5 eqeq2d ${⊢}{y}={x}\to \left({X}={y}\mathrm{ball}\left({M}\right){r}↔{X}={x}\mathrm{ball}\left({M}\right){r}\right)$
7 6 rexbidv ${⊢}{y}={x}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$
8 7 rspcva ${⊢}\left({x}\in {X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}$
9 4 8 sylan ${⊢}\left(\left({x}\in {S}\wedge {S}\subseteq {X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}$
10 9 adantlll ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}$
11 dfss ${⊢}{S}\subseteq {X}↔{S}={S}\cap {X}$
12 11 biimpi ${⊢}{S}\subseteq {X}\to {S}={S}\cap {X}$
13 incom ${⊢}{S}\cap {X}={X}\cap {S}$
14 12 13 syl6eq ${⊢}{S}\subseteq {X}\to {S}={X}\cap {S}$
15 ineq1 ${⊢}{X}={x}\mathrm{ball}\left({M}\right){r}\to {X}\cap {S}=\left({x}\mathrm{ball}\left({M}\right){r}\right)\cap {S}$
16 14 15 sylan9eq ${⊢}\left({S}\subseteq {X}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\to {S}=\left({x}\mathrm{ball}\left({M}\right){r}\right)\cap {S}$
17 16 adantll ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\to {S}=\left({x}\mathrm{ball}\left({M}\right){r}\right)\cap {S}$
18 17 adantlr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\to {S}=\left({x}\mathrm{ball}\left({M}\right){r}\right)\cap {S}$
19 eqid ${⊢}{{M}↾}_{\left({S}×{S}\right)}={{M}↾}_{\left({S}×{S}\right)}$
20 19 blssp ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({x}\in {S}\wedge {r}\in {ℝ}^{+}\right)\right)\to {x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}=\left({x}\mathrm{ball}\left({M}\right){r}\right)\cap {S}$
21 20 an4s ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge \left({S}\subseteq {X}\wedge {r}\in {ℝ}^{+}\right)\right)\to {x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}=\left({x}\mathrm{ball}\left({M}\right){r}\right)\cap {S}$
22 21 anassrs ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge {r}\in {ℝ}^{+}\right)\to {x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}=\left({x}\mathrm{ball}\left({M}\right){r}\right)\cap {S}$
23 22 adantr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\to {x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}=\left({x}\mathrm{ball}\left({M}\right){r}\right)\cap {S}$
24 18 23 eqtr4d ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\to {S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}$
25 24 ex ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge {r}\in {ℝ}^{+}\right)\to \left({X}={x}\mathrm{ball}\left({M}\right){r}\to {S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}\right)$
26 25 reximdva ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}\right)$
27 26 imp ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}$
28 10 27 syldan ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}$
29 28 an32s ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\wedge {S}\subseteq {X}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}$
30 29 ex ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {S}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\to \left({S}\subseteq {X}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}\right)$
31 30 an32s ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\wedge {x}\in {S}\right)\to \left({S}\subseteq {X}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}\right)$
32 31 imp ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\wedge {x}\in {S}\right)\wedge {S}\subseteq {X}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}$
33 32 an32s ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\wedge {S}\subseteq {X}\right)\wedge {x}\in {S}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}$
34 33 ralrimiva ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\wedge {S}\subseteq {X}\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}$
35 2 34 jca ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\wedge {S}\subseteq {X}\right)\to \left({{M}↾}_{\left({S}×{S}\right)}\in \mathrm{Met}\left({S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}\right)$
36 isbnd ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)$
37 36 anbi1i ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {S}\subseteq {X}\right)↔\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)\wedge {S}\subseteq {X}\right)$
38 isbnd ${⊢}{{M}↾}_{\left({S}×{S}\right)}\in \mathrm{Bnd}\left({S}\right)↔\left({{M}↾}_{\left({S}×{S}\right)}\in \mathrm{Met}\left({S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{S}={x}\mathrm{ball}\left({{M}↾}_{\left({S}×{S}\right)}\right){r}\right)$
39 35 37 38 3imtr4i ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {S}\subseteq {X}\right)\to {{M}↾}_{\left({S}×{S}\right)}\in \mathrm{Bnd}\left({S}\right)$