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 = ( Base ` M )
	mscl.d	|- D = ( dist ` M )
Assertion	xmsxmet2	|- ( M e. *MetSp -> ( D |` ( X X. X ) ) e. ( *Met ` X ) )

Proof

Step	Hyp	Ref	Expression
1		mscl.x	|- X = ( Base ` M )
2		mscl.d	|- D = ( dist ` M )
3	2	reseq1i	|- ( D |` ( X X. X ) ) = ( ( dist ` M ) |` ( X X. X ) )
4	1 3	xmsxmet	|- ( M e. *MetSp -> ( D |` ( X X. X ) ) e. ( *Met ` X ) )