This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metcl

Description: Closure of the distance function of a metric space. Part of Property M1 of Kreyszig p. 3. (Contributed by NM, 30-Aug-2006)

		Ref	Expression
	Assertion	metcl	$⊢ (D \in Met (X) \land A \in X \land B \in X) \to A D B \in ℝ$

Step	Hyp	Ref	Expression
1		metf	$⊢ D \in Met (X) \to D : X \times X ⟶ ℝ$
2		fovcdm	$⊢ (D : X \times X ⟶ ℝ \land A \in X \land B \in X) \to A D B \in ℝ$
3	1 2	syl3an1	$⊢ (D \in Met (X) \land A \in X \land B \in X) \to A D B \in ℝ$