Metamath Proof Explorer


Theorem metxmet

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

Ref Expression
Assertion metxmet DMetXD∞MetX

Proof

Step Hyp Ref Expression
1 ismet2 DMetXD∞MetXD:X×X
2 1 simplbi DMetXD∞MetX