Theorem xmettpos

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

	Ref	Expression
Assertion	xmettpos	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → tpos 𝐷 = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
2	1	3expb	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
3	2	ralrimivva	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
4		xmetf	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
5		ffn	⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → 𝐷 Fn ( 𝑋 × 𝑋 ) )
6		tpossym	⊢ ( 𝐷 Fn ( 𝑋 × 𝑋 ) → ( tpos 𝐷 = 𝐷 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) ) )
7	4 5 6	3syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( tpos 𝐷 = 𝐷 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) ) )
8	3 7	mpbird	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → tpos 𝐷 = 𝐷 )