xmettpos

Description: The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xmettpos	$⊢ D \in ∞Met (X) \to tpos D = D$

Step	Hyp	Ref	Expression
1		xmetsym	$⊢ (D \in ∞Met (X) \land x \in X \land y \in X) \to x D y = y D x$
2	1	3expb	$⊢ (D \in ∞Met (X) \land (x \in X \land y \in X)) \to x D y = y D x$
3	2	ralrimivva	$⊢ D \in ∞Met (X) \to \forall x \in X \forall y \in X x D y = y D x$
4		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
5		ffn	$⊢ D : X \times X ⟶ ℝ^{*} \to D Fn (X \times X)$
6		tpossym	$⊢ D Fn (X \times X) \to (tpos D = D \leftrightarrow \forall x \in X \forall y \in X x D y = y D x)$
7	4 5 6	3syl	$⊢ D \in ∞Met (X) \to (tpos D = D \leftrightarrow \forall x \in X \forall y \in X x D y = y D x)$
8	3 7	mpbird	$⊢ D \in ∞Met (X) \to tpos D = D$

Metamath Proof Explorer