# Metamath Proof Explorer

## Theorem isbndx

Description: A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion isbndx ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$

### Proof

Step Hyp Ref Expression
1 isbnd ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$
2 metxmet ${⊢}{M}\in \mathrm{Met}\left({X}\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
3 simpr ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\wedge {M}\in \mathrm{\infty Met}\left({X}\right)\right)\to {M}\in \mathrm{\infty Met}\left({X}\right)$
4 xmetf ${⊢}{M}\in \mathrm{\infty Met}\left({X}\right)\to {M}:{X}×{X}⟶{ℝ}^{*}$
5 ffn ${⊢}{M}:{X}×{X}⟶{ℝ}^{*}\to {M}Fn\left({X}×{X}\right)$
6 3 4 5 3syl ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\wedge {M}\in \mathrm{\infty Met}\left({X}\right)\right)\to {M}Fn\left({X}×{X}\right)$
7 simprr ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\to {X}={x}\mathrm{ball}\left({M}\right){r}$
8 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
9 eqid ${⊢}{{M}}^{-1}\left[ℝ\right]={{M}}^{-1}\left[ℝ\right]$
10 9 blssec ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to {x}\mathrm{ball}\left({M}\right){r}\subseteq \left[{x}\right]{{M}}^{-1}\left[ℝ\right]$
11 10 3expa ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge {r}\in {ℝ}^{*}\right)\to {x}\mathrm{ball}\left({M}\right){r}\subseteq \left[{x}\right]{{M}}^{-1}\left[ℝ\right]$
12 8 11 sylan2 ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge {r}\in {ℝ}^{+}\right)\to {x}\mathrm{ball}\left({M}\right){r}\subseteq \left[{x}\right]{{M}}^{-1}\left[ℝ\right]$
13 12 adantrr ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\to {x}\mathrm{ball}\left({M}\right){r}\subseteq \left[{x}\right]{{M}}^{-1}\left[ℝ\right]$
14 7 13 eqsstrd ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\to {X}\subseteq \left[{x}\right]{{M}}^{-1}\left[ℝ\right]$
15 14 sselda ${⊢}\left(\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge {y}\in {X}\right)\to {y}\in \left[{x}\right]{{M}}^{-1}\left[ℝ\right]$
16 vex ${⊢}{y}\in \mathrm{V}$
17 vex ${⊢}{x}\in \mathrm{V}$
18 16 17 elec ${⊢}{y}\in \left[{x}\right]{{M}}^{-1}\left[ℝ\right]↔{x}{{M}}^{-1}\left[ℝ\right]{y}$
19 15 18 sylib ${⊢}\left(\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge {y}\in {X}\right)\to {x}{{M}}^{-1}\left[ℝ\right]{y}$
20 9 xmeterval ${⊢}{M}\in \mathrm{\infty Met}\left({X}\right)\to \left({x}{{M}}^{-1}\left[ℝ\right]{y}↔\left({x}\in {X}\wedge {y}\in {X}\wedge {x}{M}{y}\in ℝ\right)\right)$
21 20 ad3antrrr ${⊢}\left(\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge {y}\in {X}\right)\to \left({x}{{M}}^{-1}\left[ℝ\right]{y}↔\left({x}\in {X}\wedge {y}\in {X}\wedge {x}{M}{y}\in ℝ\right)\right)$
22 19 21 mpbid ${⊢}\left(\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge {y}\in {X}\right)\to \left({x}\in {X}\wedge {y}\in {X}\wedge {x}{M}{y}\in ℝ\right)$
23 22 simp3d ${⊢}\left(\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\wedge {y}\in {X}\right)\to {x}{M}{y}\in ℝ$
24 23 ralrimiva ${⊢}\left(\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\wedge \left({r}\in {ℝ}^{+}\wedge {X}={x}\mathrm{ball}\left({M}\right){r}\right)\right)\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\in ℝ$
25 24 rexlimdvaa ${⊢}\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\in ℝ\right)$
26 25 ralimdva ${⊢}{M}\in \mathrm{\infty Met}\left({X}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\in ℝ\right)$
27 26 impcom ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\wedge {M}\in \mathrm{\infty Met}\left({X}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\in ℝ$
28 ffnov ${⊢}{M}:{X}×{X}⟶ℝ↔\left({M}Fn\left({X}×{X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\in ℝ\right)$
29 6 27 28 sylanbrc ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\wedge {M}\in \mathrm{\infty Met}\left({X}\right)\right)\to {M}:{X}×{X}⟶ℝ$
30 ismet2 ${⊢}{M}\in \mathrm{Met}\left({X}\right)↔\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge {M}:{X}×{X}⟶ℝ\right)$
31 3 29 30 sylanbrc ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\wedge {M}\in \mathrm{\infty Met}\left({X}\right)\right)\to {M}\in \mathrm{Met}\left({X}\right)$
32 31 ex ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\to \left({M}\in \mathrm{\infty Met}\left({X}\right)\to {M}\in \mathrm{Met}\left({X}\right)\right)$
33 2 32 impbid2 ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\to \left({M}\in \mathrm{Met}\left({X}\right)↔{M}\in \mathrm{\infty Met}\left({X}\right)\right)$
34 33 pm5.32ri ${⊢}\left({M}\in \mathrm{Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)↔\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$
35 1 34 bitri ${⊢}{M}\in \mathrm{Bnd}\left({X}\right)↔\left({M}\in \mathrm{\infty Met}\left({X}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{X}={x}\mathrm{ball}\left({M}\right){r}\right)$