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	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) ⊆ ( 𝑋 × 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		metidval	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } )
2		opabssxp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) } ⊆ ( 𝑋 × 𝑋 )
3	1 2	eqsstrdi	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) ⊆ ( 𝑋 × 𝑋 ) )