# Metamath Proof Explorer

## Theorem ismeti

Description: Properties that determine a metric. (Contributed by NM, 17-Nov-2006) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses ismeti.0 ${⊢}{X}\in \mathrm{V}$
ismeti.1 ${⊢}{D}:{X}×{X}⟶ℝ$
ismeti.2 ${⊢}\left({x}\in {X}\wedge {y}\in {X}\right)\to \left({x}{D}{y}=0↔{x}={y}\right)$
ismeti.3 ${⊢}\left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\to {x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)$
Assertion ismeti ${⊢}{D}\in \mathrm{Met}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 ismeti.0 ${⊢}{X}\in \mathrm{V}$
2 ismeti.1 ${⊢}{D}:{X}×{X}⟶ℝ$
3 ismeti.2 ${⊢}\left({x}\in {X}\wedge {y}\in {X}\right)\to \left({x}{D}{y}=0↔{x}={y}\right)$
4 ismeti.3 ${⊢}\left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\to {x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)$
5 4 3expa ${⊢}\left(\left({x}\in {X}\wedge {y}\in {X}\right)\wedge {z}\in {X}\right)\to {x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)$
6 5 ralrimiva ${⊢}\left({x}\in {X}\wedge {y}\in {X}\right)\to \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)$
7 3 6 jca ${⊢}\left({x}\in {X}\wedge {y}\in {X}\right)\to \left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)$
8 7 rgen2 ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)$
9 ismet ${⊢}{X}\in \mathrm{V}\to \left({D}\in \mathrm{Met}\left({X}\right)↔\left({D}:{X}×{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)\right)$
10 1 9 ax-mp ${⊢}{D}\in \mathrm{Met}\left({X}\right)↔\left({D}:{X}×{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{D}{y}=0↔{x}={y}\right)\wedge \forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{x}{D}{y}\le \left({z}{D}{x}\right)+\left({z}{D}{y}\right)\right)\right)$
11 2 8 10 mpbir2an ${⊢}{D}\in \mathrm{Met}\left({X}\right)$