# Metamath Proof Explorer

## Theorem isbnd3b

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

Ref Expression
Assertion isbnd3b ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\le {x}\right)$

### Proof

Step Hyp Ref Expression
1 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)$
2 metf ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}:{X}×{X}⟶ℝ$
3 2 adantr ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\to {M}:{X}×{X}⟶ℝ$
4 ffn ${⊢}{M}:{X}×{X}⟶ℝ\to {M}Fn\left({X}×{X}\right)$
5 ffnov ${⊢}{M}:{X}×{X}⟶\left[0,{x}\right]↔\left({M}Fn\left({X}×{X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\in \left[0,{x}\right]\right)$
6 5 baib ${⊢}{M}Fn\left({X}×{X}\right)\to \left({M}:{X}×{X}⟶\left[0,{x}\right]↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\in \left[0,{x}\right]\right)$
7 3 4 6 3syl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\to \left({M}:{X}×{X}⟶\left[0,{x}\right]↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\in \left[0,{x}\right]\right)$
8 0red ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge \left({y}\in {X}\wedge {z}\in {X}\right)\right)\to 0\in ℝ$
9 simplr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge \left({y}\in {X}\wedge {z}\in {X}\right)\right)\to {x}\in ℝ$
10 metcl ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\wedge {z}\in {X}\right)\to {y}{M}{z}\in ℝ$
11 10 3expb ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({y}\in {X}\wedge {z}\in {X}\right)\right)\to {y}{M}{z}\in ℝ$
12 11 adantlr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge \left({y}\in {X}\wedge {z}\in {X}\right)\right)\to {y}{M}{z}\in ℝ$
13 metge0 ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {y}\in {X}\wedge {z}\in {X}\right)\to 0\le {y}{M}{z}$
14 13 3expb ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \left({y}\in {X}\wedge {z}\in {X}\right)\right)\to 0\le {y}{M}{z}$
15 14 adantlr ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge \left({y}\in {X}\wedge {z}\in {X}\right)\right)\to 0\le {y}{M}{z}$
16 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)$
17 df-3an ${⊢}\left({y}{M}{z}\in ℝ\wedge 0\le {y}{M}{z}\wedge {y}{M}{z}\le {x}\right)↔\left(\left({y}{M}{z}\in ℝ\wedge 0\le {y}{M}{z}\right)\wedge {y}{M}{z}\le {x}\right)$
18 16 17 syl6bb ${⊢}\left(0\in ℝ\wedge {x}\in ℝ\right)\to \left({y}{M}{z}\in \left[0,{x}\right]↔\left(\left({y}{M}{z}\in ℝ\wedge 0\le {y}{M}{z}\right)\wedge {y}{M}{z}\le {x}\right)\right)$
19 18 baibd ${⊢}\left(\left(0\in ℝ\wedge {x}\in ℝ\right)\wedge \left({y}{M}{z}\in ℝ\wedge 0\le {y}{M}{z}\right)\right)\to \left({y}{M}{z}\in \left[0,{x}\right]↔{y}{M}{z}\le {x}\right)$
20 8 9 12 15 19 syl22anc ${⊢}\left(\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\wedge \left({y}\in {X}\wedge {z}\in {X}\right)\right)\to \left({y}{M}{z}\in \left[0,{x}\right]↔{y}{M}{z}\le {x}\right)$
21 20 2ralbidva ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\in \left[0,{x}\right]↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\le {x}\right)$
22 7 21 bitrd ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge {x}\in ℝ\right)\to \left({M}:{X}×{X}⟶\left[0,{x}\right]↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\le {x}\right)$
23 22 rexbidva ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\le {x}\right)$
24 23 pm5.32i ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{M}:{X}×{X}⟶\left[0,{x}\right]\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\le {x}\right)$
25 1 24 bitri ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{y}{M}{z}\le {x}\right)$