Theorem metxmet

Description: A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ismet2	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
2	1	simplbi	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )