# Metamath Proof Explorer

## Theorem isbnd3

Description: A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Assertion isbnd3 ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)$

### Proof

Step Hyp Ref Expression
1 bndmet ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to {M}\in \mathrm{Met}\left({X}\right)$
2 0re ${⊢}0\in ℝ$
3 2 ne0ii ${⊢}ℝ\ne \varnothing$
4 metf ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}:{X}×{X}⟶ℝ$
5 4 ffnd ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}Fn\left({X}×{X}\right)$
6 1 5 syl ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to {M}Fn\left({X}×{X}\right)$
7 6 ad2antrr ${⊢}\left(\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}=\varnothing \right)\wedge {x}\in ℝ\right)\to {M}Fn\left({X}×{X}\right)$
8 1 4 syl ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to {M}:{X}×{X}⟶ℝ$
9 8 fdmd ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to \mathrm{dom}{M}={X}×{X}$
10 xpeq2 ${⊢}{X}=\varnothing \to {X}×{X}={X}×\varnothing$
11 xp0 ${⊢}{X}×\varnothing =\varnothing$
12 10 11 syl6eq ${⊢}{X}=\varnothing \to {X}×{X}=\varnothing$
13 9 12 sylan9eq ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}=\varnothing \right)\to \mathrm{dom}{M}=\varnothing$
14 13 adantr ${⊢}\left(\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}=\varnothing \right)\wedge {x}\in ℝ\right)\to \mathrm{dom}{M}=\varnothing$
15 dm0rn0 ${⊢}\mathrm{dom}{M}=\varnothing ↔\mathrm{ran}{M}=\varnothing$
16 14 15 sylib ${⊢}\left(\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}=\varnothing \right)\wedge {x}\in ℝ\right)\to \mathrm{ran}{M}=\varnothing$
17 0ss ${⊢}\varnothing \subseteq \left[0,{x}\right]$
18 16 17 eqsstrdi ${⊢}\left(\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}=\varnothing \right)\wedge {x}\in ℝ\right)\to \mathrm{ran}{M}\subseteq \left[0,{x}\right]$
19 df-f ${⊢}{M}:{X}×{X}⟶\left[0,{x}\right]↔\left({M}Fn\left({X}×{X}\right)\wedge \mathrm{ran}{M}\subseteq \left[0,{x}\right]\right)$
20 7 18 19 sylanbrc ${⊢}\left(\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}=\varnothing \right)\wedge {x}\in ℝ\right)\to {M}:{X}×{X}⟶\left[0,{x}\right]$
21 20 ralrimiva ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}=\varnothing \right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]$
22 r19.2z ${⊢}\left(ℝ\ne \varnothing \wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]$
23 3 21 22 sylancr ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}=\varnothing \right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]$
24 isbnd2 ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}\ne \varnothing \right)↔\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\right)$
25 24 simprbi ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}\ne \varnothing \right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}$
26 2re ${⊢}2\in ℝ$
27 simprlr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\to {r}\in {ℝ}^{+}$
28 27 rpred ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\to {r}\in ℝ$
29 remulcl ${⊢}\left(2\in ℝ\wedge {r}\in ℝ\right)\to 2{r}\in ℝ$
30 26 28 29 sylancr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\to 2{r}\in ℝ$
31 5 adantr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\to {M}Fn\left({X}×{X}\right)$
32 simpll ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {M}\in \mathrm{Met}\left({X}\right)$
33 simprl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {x}\in {X}$
34 simprr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {z}\in {X}$
35 metcl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {X}\wedge {z}\in {X}\right)\to {x}{M}{z}\in ℝ$
36 32 33 34 35 syl3anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {x}{M}{z}\in ℝ$
37 metge0 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in {X}\wedge {z}\in {X}\right)\to 0\le {x}{M}{z}$
38 32 33 34 37 syl3anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to 0\le {x}{M}{z}$
39 30 adantr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to 2{r}\in ℝ$
40 simprll ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\to {y}\in {X}$
41 40 adantr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {y}\in {X}$
42 metcl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\wedge {x}\in {X}\right)\to {y}{M}{x}\in ℝ$
43 32 41 33 42 syl3anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {y}{M}{x}\in ℝ$
44 metcl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\wedge {z}\in {X}\right)\to {y}{M}{z}\in ℝ$
45 32 41 34 44 syl3anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {y}{M}{z}\in ℝ$
46 43 45 readdcld ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to \left({y}{M}{x}\right)+\left({y}{M}{z}\right)\in ℝ$
47 mettri2 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({y}\in {X}\wedge {x}\in {X}\wedge {z}\in {X}\right)\right)\to {x}{M}{z}\le \left({y}{M}{x}\right)+\left({y}{M}{z}\right)$
48 32 41 33 34 47 syl13anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {x}{M}{z}\le \left({y}{M}{x}\right)+\left({y}{M}{z}\right)$
49 28 adantr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {r}\in ℝ$
50 simplrr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {X}={y}\mathrm{ball}\left({M}\right){r}$
51 33 50 eleqtrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {x}\in \left({y}\mathrm{ball}\left({M}\right){r}\right)$
52 metxmet ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
53 32 52 syl ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
54 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
55 54 ad2antlr ${⊢}\left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\to {r}\in {ℝ}^{*}$
56 55 ad2antlr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {r}\in {ℝ}^{*}$
57 elbl2 ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {r}\in {ℝ}^{*}\right)\wedge \left({y}\in {X}\wedge {x}\in {X}\right)\right)\to \left({x}\in \left({y}\mathrm{ball}\left({M}\right){r}\right)↔{y}{M}{x}<{r}\right)$
58 53 56 41 33 57 syl22anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to \left({x}\in \left({y}\mathrm{ball}\left({M}\right){r}\right)↔{y}{M}{x}<{r}\right)$
59 51 58 mpbid ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {y}{M}{x}<{r}$
60 34 50 eleqtrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {z}\in \left({y}\mathrm{ball}\left({M}\right){r}\right)$
61 elbl2 ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {r}\in {ℝ}^{*}\right)\wedge \left({y}\in {X}\wedge {z}\in {X}\right)\right)\to \left({z}\in \left({y}\mathrm{ball}\left({M}\right){r}\right)↔{y}{M}{z}<{r}\right)$
62 53 56 41 34 61 syl22anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to \left({z}\in \left({y}\mathrm{ball}\left({M}\right){r}\right)↔{y}{M}{z}<{r}\right)$
63 60 62 mpbid ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {y}{M}{z}<{r}$
64 43 45 49 49 59 63 lt2addd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to \left({y}{M}{x}\right)+\left({y}{M}{z}\right)<{r}+{r}$
65 49 recnd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {r}\in ℂ$
66 65 2timesd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to 2{r}={r}+{r}$
67 64 66 breqtrrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to \left({y}{M}{x}\right)+\left({y}{M}{z}\right)<2{r}$
68 36 46 39 48 67 lelttrd ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {x}{M}{z}<2{r}$
69 36 39 68 ltled ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {x}{M}{z}\le 2{r}$
70 elicc2 ${⊢}\left(0\in ℝ\wedge 2{r}\in ℝ\right)\to \left({x}{M}{z}\in \left[0,2{r}\right]↔\left({x}{M}{z}\in ℝ\wedge 0\le {x}{M}{z}\wedge {x}{M}{z}\le 2{r}\right)\right)$
71 2 39 70 sylancr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to \left({x}{M}{z}\in \left[0,2{r}\right]↔\left({x}{M}{z}\in ℝ\wedge 0\le {x}{M}{z}\wedge {x}{M}{z}\le 2{r}\right)\right)$
72 36 38 69 71 mpbir3and ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\right)\to {x}{M}{z}\in \left[0,2{r}\right]$
73 72 ralrimivva ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{z}\in \left[0,2{r}\right]$
74 ffnov ${⊢}{M}:{X}×{X}⟶\left[0,2{r}\right]↔\left({M}Fn\left({X}×{X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{z}\in \left[0,2{r}\right]\right)$
75 31 73 74 sylanbrc ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\to {M}:{X}×{X}⟶\left[0,2{r}\right]$
76 oveq2 ${⊢}{x}=2{r}\to \left[0,{x}\right]=\left[0,2{r}\right]$
77 76 feq3d ${⊢}{x}=2{r}\to \left({M}:{X}×{X}⟶\left[0,{x}\right]↔{M}:{X}×{X}⟶\left[0,2{r}\right]\right)$
78 77 rspcev ${⊢}\left(2{r}\in ℝ\wedge {M}:{X}×{X}⟶\left[0,2{r}\right]\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]$
79 30 75 78 syl2anc ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left(\left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\wedge {X}={y}\mathrm{ball}\left({M}\right){r}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]$
80 79 expr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({y}\in {X}\wedge {r}\in {ℝ}^{+}\right)\right)\to \left({X}={y}\mathrm{ball}\left({M}\right){r}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)$
81 80 rexlimdvva ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)$
82 1 81 syl ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)$
83 82 adantr ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}\ne \varnothing \right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)$
84 25 83 mpd ${⊢}\left({M}\in \mathrm{Bnd}\left({X}\right)\wedge {X}\ne \varnothing \right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]$
85 23 84 pm2.61dane ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]$
86 1 85 jca ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)\to \left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)$
87 simpll ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\to {M}\in \mathrm{Met}\left({X}\right)$
88 simpllr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {x}\in ℝ$
89 87 adantr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {M}\in \mathrm{Met}\left({X}\right)$
90 simpr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {y}\in {X}$
91 met0 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\right)\to {y}{M}{y}=0$
92 89 90 91 syl2anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {y}{M}{y}=0$
93 simplr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {M}:{X}×{X}⟶\left[0,{x}\right]$
94 93 90 90 fovrnd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {y}{M}{y}\in \left[0,{x}\right]$
95 elicc2 ${⊢}\left(0\in ℝ\wedge {x}\in ℝ\right)\to \left({y}{M}{y}\in \left[0,{x}\right]↔\left({y}{M}{y}\in ℝ\wedge 0\le {y}{M}{y}\wedge {y}{M}{y}\le {x}\right)\right)$
96 2 88 95 sylancr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to \left({y}{M}{y}\in \left[0,{x}\right]↔\left({y}{M}{y}\in ℝ\wedge 0\le {y}{M}{y}\wedge {y}{M}{y}\le {x}\right)\right)$
97 94 96 mpbid ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to \left({y}{M}{y}\in ℝ\wedge 0\le {y}{M}{y}\wedge {y}{M}{y}\le {x}\right)$
98 97 simp3d ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {y}{M}{y}\le {x}$
99 92 98 eqbrtrrd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to 0\le {x}$
100 88 99 ge0p1rpd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {x}+1\in {ℝ}^{+}$
101 fovrn ${⊢}\left({M}:{X}×{X}⟶\left[0,{x}\right]\wedge {y}\in {X}\wedge {z}\in {X}\right)\to {y}{M}{z}\in \left[0,{x}\right]$
102 101 3expa ${⊢}\left(\left({M}:{X}×{X}⟶\left[0,{x}\right]\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {y}{M}{z}\in \left[0,{x}\right]$
103 102 adantlll ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {y}{M}{z}\in \left[0,{x}\right]$
104 elicc2 ${⊢}\left(0\in ℝ\wedge {x}\in ℝ\right)\to \left({y}{M}{z}\in \left[0,{x}\right]↔\left({y}{M}{z}\in ℝ\wedge 0\le {y}{M}{z}\wedge {y}{M}{z}\le {x}\right)\right)$
105 2 88 104 sylancr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to \left({y}{M}{z}\in \left[0,{x}\right]↔\left({y}{M}{z}\in ℝ\wedge 0\le {y}{M}{z}\wedge {y}{M}{z}\le {x}\right)\right)$
106 105 adantr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to \left({y}{M}{z}\in \left[0,{x}\right]↔\left({y}{M}{z}\in ℝ\wedge 0\le {y}{M}{z}\wedge {y}{M}{z}\le {x}\right)\right)$
107 103 106 mpbid ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to \left({y}{M}{z}\in ℝ\wedge 0\le {y}{M}{z}\wedge {y}{M}{z}\le {x}\right)$
108 107 simp1d ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {y}{M}{z}\in ℝ$
109 88 adantr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {x}\in ℝ$
110 peano2re ${⊢}{x}\in ℝ\to {x}+1\in ℝ$
111 88 110 syl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {x}+1\in ℝ$
112 111 adantr ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {x}+1\in ℝ$
113 107 simp3d ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {y}{M}{z}\le {x}$
114 109 ltp1d ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {x}<{x}+1$
115 108 109 112 113 114 lelttrd ${⊢}\left(\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {y}{M}{z}<{x}+1$
116 115 ralrimiva ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}<{x}+1$
117 rabid2 ${⊢}{X}=\left\{{z}\in {X}|{y}{M}{z}<{x}+1\right\}↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}<{x}+1$
118 116 117 sylibr ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {X}=\left\{{z}\in {X}|{y}{M}{z}<{x}+1\right\}$
119 89 52 syl ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
120 111 rexrd ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {x}+1\in {ℝ}^{*}$
121 blval ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {x}+1\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({M}\right)\left({x}+1\right)=\left\{{z}\in {X}|{y}{M}{z}<{x}+1\right\}$
122 119 90 120 121 syl3anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {y}\mathrm{ball}\left({M}\right)\left({x}+1\right)=\left\{{z}\in {X}|{y}{M}{z}<{x}+1\right\}$
123 118 122 eqtr4d ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to {X}={y}\mathrm{ball}\left({M}\right)\left({x}+1\right)$
124 oveq2 ${⊢}{r}={x}+1\to {y}\mathrm{ball}\left({M}\right){r}={y}\mathrm{ball}\left({M}\right)\left({x}+1\right)$
125 124 rspceeqv ${⊢}\left({x}+1\in {ℝ}^{+}\wedge {X}={y}\mathrm{ball}\left({M}\right)\left({x}+1\right)\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}$
126 100 123 125 syl2anc ${⊢}\left(\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\wedge {y}\in {X}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}$
127 126 ralrimiva ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={y}\mathrm{ball}\left({M}\right){r}$
128 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)$
129 87 127 128 sylanbrc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge {M}:{X}×{X}⟶\left[0,{x}\right]\right)\to {M}\in \mathrm{Bnd}\left({X}\right)$
130 129 r19.29an ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)\to {M}\in \mathrm{Bnd}\left({X}\right)$
131 86 130 impbii ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)$