Theorem rexmet

Description: The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypothesis	remet.1	|- D = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion	rexmet	|- D e. ( *Met ` RR )

Proof

Step	Hyp	Ref	Expression
1		remet.1	|- D = ( ( abs o. - ) |` ( RR X. RR ) )
2	1	remet	|- D e. ( Met ` RR )
3		metxmet	|- ( D e. ( Met ` RR ) -> D e. ( *Met ` RR ) )
4	2 3	ax-mp	|- D e. ( *Met ` RR )