Theorem psmetf

Description: The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018)

	Ref	Expression
Assertion	psmetf	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
2		ispsmet	⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) ) ) )
3	1 2	syl	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) ) ) )
4	3	ibi	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑎 ∈ 𝑋 ( ( 𝑎 𝐷 𝑎 ) = 0 ∧ ∀ 𝑏 ∈ 𝑋 ∀ 𝑐 ∈ 𝑋 ( 𝑎 𝐷 𝑏 ) ≤ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) ) )
5	4	simpld	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )