Metamath Proof Explorer


Theorem xmsxmet2

Description: The distance function, suitably truncated, is an extended metric on X . (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mscl.x X=BaseM
mscl.d D=distM
Assertion xmsxmet2 M∞MetSpDX×X∞MetX

Proof

Step Hyp Ref Expression
1 mscl.x X=BaseM
2 mscl.d D=distM
3 2 reseq1i DX×X=distMX×X
4 1 3 xmsxmet M∞MetSpDX×X∞MetX