Theorem metpsmet

Description: A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Assertion	metpsmet	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \mathrm{PsMet}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		metxmet	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \mathrm{\infty Met}\left(X\right)$$
2		xmetpsmet	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D\in \mathrm{PsMet}\left(X\right)$$
3	1 2	syl	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \mathrm{PsMet}\left(X\right)$$