isxmetd

Description: Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by AV, 9-Apr-2024)

	Ref	Expression
Hypotheses	isxmetd.0	$⊢ φ \to X \in V$
	isxmetd.1	$⊢ φ \to D : X \times X ⟶ ℝ^{*}$
	isxmetd.2	$⊢ (φ \land (x \in X \land y \in X)) \to (x D y = 0 \leftrightarrow x = y)$
	isxmetd.3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x D y \leq (z D x) +_{𝑒} (z D y)$
Assertion	isxmetd	$⊢ φ \to D \in ∞Met (X)$

Step	Hyp	Ref	Expression
1		isxmetd.0	$⊢ φ \to X \in V$
2		isxmetd.1	$⊢ φ \to D : X \times X ⟶ ℝ^{*}$
3		isxmetd.2	$⊢ (φ \land (x \in X \land y \in X)) \to (x D y = 0 \leftrightarrow x = y)$
4		isxmetd.3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x D y \leq (z D x) +_{𝑒} (z D y)$
5	4	3exp2	$⊢ φ \to (x \in X \to (y \in X \to (z \in X \to x D y \leq (z D x) +_{𝑒} (z D y))))$
6	5	imp32	$⊢ (φ \land (x \in X \land y \in X)) \to (z \in X \to x D y \leq (z D x) +_{𝑒} (z D y))$
7	6	ralrimiv	$⊢ (φ \land (x \in X \land y \in X)) \to \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y)$
8	3 7	jca	$⊢ (φ \land (x \in X \land y \in X)) \to ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))$
9	8	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))$
10		isxmet	$⊢ X \in V \to (D \in ∞Met (X) \leftrightarrow (D : X \times X ⟶ ℝ^{*} \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$
11	1 10	syl	$⊢ φ \to (D \in ∞Met (X) \leftrightarrow (D : X \times X ⟶ ℝ^{*} \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$
12	2 9 11	mpbir2and	$⊢ φ \to D \in ∞Met (X)$

Metamath Proof Explorer