Theorem msmet2

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

	Ref	Expression
Hypotheses	mscl.x	|- X = ( Base ` M )
	mscl.d	|- D = ( dist ` M )
Assertion	msmet2	|- ( 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	msmet	|- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) )