Metamath Proof Explorer

Theorem metidss

Description: As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018)

		Ref	Expression
	Assertion	metidss	\|- ( D e. ( PsMet ` X ) -> ( ~Met ` D ) C_ ( X X. X ) )

Step	Hyp	Ref	Expression
1		metidval	\|- ( D e. ( PsMet ` X ) -> ( ~Met ` D ) = { <. x , y >. \| ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } )
2		opabssxp	\|- { <. x , y >. \| ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } C_ ( X X. X )
3	1 2	eqsstrdi	\|- ( D e. ( PsMet ` X ) -> ( ~Met ` D ) C_ ( X X. X ) )

Step

Hyp

Ref

Expression

 |-  ( D e. ( PsMet ` X ) -> ( ~Met ` D ) = { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } )

 |-  { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } C_ ( X X. X )

1 2

 |-  ( D e. ( PsMet ` X ) -> ( ~Met ` D ) C_ ( X X. X ) )