# Metamath Proof Explorer

## Theorem metdsle

Description: The distance from a point to a set is bounded by the distance to any member of the set. (Contributed by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypothesis metdscn.f ${⊢}{F}=\left({x}\in {X}⟼sup\left(\mathrm{ran}\left({y}\in {S}⟼{x}{D}{y}\right),{ℝ}^{*},<\right)\right)$
Assertion metdsle ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {F}\left({B}\right)\le {A}{D}{B}$

### Proof

Step Hyp Ref Expression
1 metdscn.f ${⊢}{F}=\left({x}\in {X}⟼sup\left(\mathrm{ran}\left({y}\in {S}⟼{x}{D}{y}\right),{ℝ}^{*},<\right)\right)$
2 simprr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {B}\in {X}$
3 simpr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\to {S}\subseteq {X}$
4 3 sselda ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge {A}\in {S}\right)\to {A}\in {X}$
5 4 adantrr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {A}\in {X}$
6 2 5 jca ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to \left({B}\in {X}\wedge {A}\in {X}\right)$
7 1 metdstri ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({B}\in {X}\wedge {A}\in {X}\right)\right)\to {F}\left({B}\right)\le \left({B}{D}{A}\right){+}_{𝑒}{F}\left({A}\right)$
8 6 7 syldan ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {F}\left({B}\right)\le \left({B}{D}{A}\right){+}_{𝑒}{F}\left({A}\right)$
9 simpll ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
10 xmetsym ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {B}\in {X}\wedge {A}\in {X}\right)\to {B}{D}{A}={A}{D}{B}$
11 9 2 5 10 syl3anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {B}{D}{A}={A}{D}{B}$
12 1 metds0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\wedge {A}\in {S}\right)\to {F}\left({A}\right)=0$
13 12 3expa ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge {A}\in {S}\right)\to {F}\left({A}\right)=0$
14 13 adantrr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {F}\left({A}\right)=0$
15 11 14 oveq12d ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to \left({B}{D}{A}\right){+}_{𝑒}{F}\left({A}\right)=\left({A}{D}{B}\right){+}_{𝑒}0$
16 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}\in {ℝ}^{*}$
17 9 5 2 16 syl3anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {A}{D}{B}\in {ℝ}^{*}$
18 17 xaddid1d ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to \left({A}{D}{B}\right){+}_{𝑒}0={A}{D}{B}$
19 15 18 eqtrd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to \left({B}{D}{A}\right){+}_{𝑒}{F}\left({A}\right)={A}{D}{B}$
20 8 19 breqtrd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {S}\subseteq {X}\right)\wedge \left({A}\in {S}\wedge {B}\in {X}\right)\right)\to {F}\left({B}\right)\le {A}{D}{B}$