Theorem 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 \mathrm{\infty Met}\left(X\right)\to tposD=D$$

Proof

Step	Hyp	Ref	Expression
1		xmetsym	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge x\in X\wedge y\in X\right)\to xDy=yDx$$
2	1	3expb	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(x\in X\wedge y\in X\right)\right)\to xDy=yDx$$
3	2	ralrimivva	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \forall x\in X\forall y\in XxDy=yDx$$
4		xmetf	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D:X\times X⟶{ℝ}^{*}$$
5		ffn	$$⊢D:X\times X⟶{ℝ}^{*}\to DFn\left(X\times X\right)$$
6		tpossym	$$⊢DFn\left(X\times X\right)\to \left(tposD=D\leftrightarrow \forall x\in X\forall y\in XxDy=yDx\right)$$
7	4 5 6	3syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(tposD=D\leftrightarrow \forall x\in X\forall y\in XxDy=yDx\right)$$
8	3 7	mpbird	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to tposD=D$$