# Metamath Proof Explorer

## Theorem totbndss

Description: A subset of a totally bounded metric space is totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

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

### Proof

Step Hyp Ref Expression
1 istotbnd ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {v}={X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
2 1 simprbi ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {v}={X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
3 sseq2 ${⊢}\bigcup {v}={X}\to \left({S}\subseteq \bigcup {v}↔{S}\subseteq {X}\right)$
4 3 biimprcd ${⊢}{S}\subseteq {X}\to \left(\bigcup {v}={X}\to {S}\subseteq \bigcup {v}\right)$
5 4 anim1d ${⊢}{S}\subseteq {X}\to \left(\left(\bigcup {v}={X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\to \left({S}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
6 5 reximdv ${⊢}{S}\subseteq {X}\to \left(\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {v}={X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\to \exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
7 6 ralimdv ${⊢}{S}\subseteq {X}\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left(\bigcup {v}={X}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
8 2 7 mpan9 ${⊢}\left({M}\in \mathrm{TotBnd}\left({X}\right)\wedge {S}\subseteq {X}\right)\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)$
9 totbndmet ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to {M}\in \mathrm{Met}\left({X}\right)$
10 eqid ${⊢}{{M}↾}_{\left({S}×{S}\right)}={{M}↾}_{\left({S}×{S}\right)}$
11 10 sstotbnd ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\to \left({{M}↾}_{\left({S}×{S}\right)}\in \mathrm{TotBnd}\left({S}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
12 9 11 sylan ${⊢}\left({M}\in \mathrm{TotBnd}\left({X}\right)\wedge {S}\subseteq {X}\right)\to \left({{M}↾}_{\left({S}×{S}\right)}\in \mathrm{TotBnd}\left({S}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {v}\wedge \forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{b}={x}\mathrm{ball}\left({M}\right){d}\right)\right)$
13 8 12 mpbird ${⊢}\left({M}\in \mathrm{TotBnd}\left({X}\right)\wedge {S}\subseteq {X}\right)\to {{M}↾}_{\left({S}×{S}\right)}\in \mathrm{TotBnd}\left({S}\right)$