Theorem metpsmet

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

	Ref	Expression
Assertion	metpsmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2		xmetpsmet	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
3	1 2	syl	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )