# Metamath Proof Explorer

## Theorem totbndbnd

Description: A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd to only require that M be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +oo ) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion totbndbnd ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to {M}\in \mathrm{Bnd}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 totbndmet ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to {M}\in \mathrm{Met}\left({X}\right)$
2 1rp ${⊢}1\in {ℝ}^{+}$
3 istotbnd3 ${⊢}{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 \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\right)$
4 3 simprbi ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}$
5 oveq2 ${⊢}{d}=1\to {x}\mathrm{ball}\left({M}\right){d}={x}\mathrm{ball}\left({M}\right)1$
6 5 iuneq2d ${⊢}{d}=1\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)=\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)$
7 6 eqeq1d ${⊢}{d}=1\to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}↔\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)$
8 7 rexbidv ${⊢}{d}=1\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}↔\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)$
9 8 rspcv ${⊢}1\in {ℝ}^{+}\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){d}\right)={X}\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)$
10 2 4 9 mpsyl ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to \exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}$
11 simplll ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to {M}\in \mathrm{Met}\left({X}\right)$
12 elfpw ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)↔\left({v}\subseteq {X}\wedge {v}\in \mathrm{Fin}\right)$
13 12 simplbi ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {v}\subseteq {X}$
14 13 ad2antrl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to {v}\subseteq {X}$
15 14 sselda ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to {z}\in {X}$
16 simpllr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to {y}\in {X}$
17 metcl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {z}\in {X}\wedge {y}\in {X}\right)\to {z}{M}{y}\in ℝ$
18 11 15 16 17 syl3anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to {z}{M}{y}\in ℝ$
19 metge0 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {z}\in {X}\wedge {y}\in {X}\right)\to 0\le {z}{M}{y}$
20 11 15 16 19 syl3anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to 0\le {z}{M}{y}$
21 18 20 ge0p1rpd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to \left({z}{M}{y}\right)+1\in {ℝ}^{+}$
22 21 fmpttd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right):{v}⟶{ℝ}^{+}$
23 22 frnd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\subseteq {ℝ}^{+}$
24 12 simprbi ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to {v}\in \mathrm{Fin}$
25 mptfi ${⊢}{v}\in \mathrm{Fin}\to \left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}$
26 rnfi ${⊢}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}$
27 24 25 26 3syl ${⊢}{v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}$
28 27 ad2antrl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}$
29 simplr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to {y}\in {X}$
30 simprr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}$
31 29 30 eleqtrrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to {y}\in \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)$
32 ne0i ${⊢}{y}\in \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)\ne \varnothing$
33 dm0rn0 ${⊢}\mathrm{dom}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)=\varnothing ↔\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)=\varnothing$
34 ovex ${⊢}\left({z}{M}{y}\right)+1\in \mathrm{V}$
35 eqid ${⊢}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)=\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
36 34 35 dmmpti ${⊢}\mathrm{dom}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)={v}$
37 36 eqeq1i ${⊢}\mathrm{dom}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)=\varnothing ↔{v}=\varnothing$
38 iuneq1 ${⊢}{v}=\varnothing \to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)=\bigcup _{{x}\in \varnothing }\left({x}\mathrm{ball}\left({M}\right)1\right)$
39 37 38 sylbi ${⊢}\mathrm{dom}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)=\varnothing \to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)=\bigcup _{{x}\in \varnothing }\left({x}\mathrm{ball}\left({M}\right)1\right)$
40 0iun ${⊢}\bigcup _{{x}\in \varnothing }\left({x}\mathrm{ball}\left({M}\right)1\right)=\varnothing$
41 39 40 syl6eq ${⊢}\mathrm{dom}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)=\varnothing \to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)=\varnothing$
42 33 41 sylbir ${⊢}\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)=\varnothing \to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)=\varnothing$
43 42 necon3i ${⊢}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)\ne \varnothing \to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\ne \varnothing$
44 31 32 43 3syl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\ne \varnothing$
45 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
46 23 45 sstrdi ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\subseteq ℝ$
47 ltso ${⊢}<\mathrm{Or}ℝ$
48 fisupcl ${⊢}\left(<\mathrm{Or}ℝ\wedge \left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}\wedge \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\ne \varnothing \wedge \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\subseteq ℝ\right)\right)\to sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
49 47 48 mpan ${⊢}\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}\wedge \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\ne \varnothing \wedge \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\subseteq ℝ\right)\to sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
50 28 44 46 49 syl3anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
51 23 50 sseldd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in {ℝ}^{+}$
52 metxmet ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
53 52 ad2antrr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
54 53 adantr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
55 1red ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to 1\in ℝ$
56 46 50 sseldd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in ℝ$
57 56 adantr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in ℝ$
58 46 adantr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\subseteq ℝ$
59 44 adantr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\ne \varnothing$
60 28 adantr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}$
61 fimaxre2 ${⊢}\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\subseteq ℝ\wedge \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\in \mathrm{Fin}\right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\phantom{\rule{.4em}{0ex}}{w}\le {d}$
62 58 60 61 syl2anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\phantom{\rule{.4em}{0ex}}{w}\le {d}$
63 35 elrnmpt1 ${⊢}\left({z}\in {v}\wedge \left({z}{M}{y}\right)+1\in \mathrm{V}\right)\to \left({z}{M}{y}\right)+1\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
64 34 63 mpan2 ${⊢}{z}\in {v}\to \left({z}{M}{y}\right)+1\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
65 64 adantl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to \left({z}{M}{y}\right)+1\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
66 suprub ${⊢}\left(\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\subseteq ℝ\wedge \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\ne \varnothing \wedge \exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\phantom{\rule{.4em}{0ex}}{w}\le {d}\right)\wedge \left({z}{M}{y}\right)+1\in \mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)\right)\to \left({z}{M}{y}\right)+1\le sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
67 58 59 62 65 66 syl31anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to \left({z}{M}{y}\right)+1\le sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
68 leaddsub ${⊢}\left({z}{M}{y}\in ℝ\wedge 1\in ℝ\wedge sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in ℝ\right)\to \left(\left({z}{M}{y}\right)+1\le sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)↔{z}{M}{y}\le sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)-1\right)$
69 18 55 57 68 syl3anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to \left(\left({z}{M}{y}\right)+1\le sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)↔{z}{M}{y}\le sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)-1\right)$
70 67 69 mpbid ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to {z}{M}{y}\le sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)-1$
71 blss2 ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {z}\in {X}\wedge {y}\in {X}\right)\wedge \left(1\in ℝ\wedge sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in ℝ\wedge {z}{M}{y}\le sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)-1\right)\right)\to {z}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
72 54 15 16 55 57 70 71 syl33anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\wedge {z}\in {v}\right)\to {z}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
73 72 ralrimiva ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \forall {z}\in {v}\phantom{\rule{.4em}{0ex}}{z}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
74 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{ball}\left({M}\right)1\right)$
75 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{y}$
76 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\mathrm{ball}\left({M}\right)$
77 nfmpt1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
78 77 nfrn ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right)$
79 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}ℝ$
80 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}<$
81 78 79 80 nfsup ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
82 75 76 81 nfov ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\right)$
83 74 82 nfss ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
84 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
85 oveq1 ${⊢}{x}={z}\to {x}\mathrm{ball}\left({M}\right)1={z}\mathrm{ball}\left({M}\right)1$
86 85 sseq1d ${⊢}{x}={z}\to \left({x}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)↔{z}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\right)$
87 83 84 86 cbvralw ${⊢}\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)↔\forall {z}\in {v}\phantom{\rule{.4em}{0ex}}{z}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
88 73 87 sylibr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
89 iunss ${⊢}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)↔\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({M}\right)1\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
90 88 89 sylibr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
91 30 90 eqsstrrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to {X}\subseteq {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
92 51 rpxrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in {ℝ}^{*}$
93 blssm ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\subseteq {X}$
94 53 29 92 93 syl3anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to {y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\subseteq {X}$
95 91 94 eqssd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to {X}={y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
96 oveq2 ${⊢}{d}=sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\to {y}\mathrm{ball}\left({M}\right){d}={y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)$
97 96 rspceeqv ${⊢}\left(sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\in {ℝ}^{+}\wedge {X}={y}\mathrm{ball}\left({M}\right)sup\left(\mathrm{ran}\left({z}\in {v}⟼\left({z}{M}{y}\right)+1\right),ℝ,<\right)\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){d}$
98 51 95 97 syl2anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge \left({v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\right)\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){d}$
99 98 rexlimdvaa ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){d}\right)$
100 99 ralrimdva ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){d}\right)$
101 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 {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){d}\right)$
102 101 baib ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left({M}\in \mathrm{Bnd}\left({X}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){d}\right)$
103 100 102 sylibrd ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\exists {v}\in \left(𝒫{X}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right)1\right)={X}\to {M}\in \mathrm{Bnd}\left({X}\right)\right)$
104 1 10 103 sylc ${⊢}{M}\in \mathrm{TotBnd}\left({X}\right)\to {M}\in \mathrm{Bnd}\left({X}\right)$