Metamath Proof Explorer


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 β€˜ 𝑋 ) )