This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psmetxrge0

Description: The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018)

Ref Expression
Assertion psmetxrge0 ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 psmetf ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
2 1 ffnd ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 Fn ( 𝑋 × 𝑋 ) )
3 1 ffvelcdmda ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝐷 ‘ 𝑎 ) ∈ ℝ* )
4 elxp6 ⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) ↔ ( 𝑎 = ⟨ ( 1st ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ ∧ ( ( 1st ‘ 𝑎 ) ∈ 𝑋 ∧ ( 2nd ‘ 𝑎 ) ∈ 𝑋 ) ) )
5 4 simprbi ⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) → ( ( 1st ‘ 𝑎 ) ∈ 𝑋 ∧ ( 2nd ‘ 𝑎 ) ∈ 𝑋 ) )
6 psmetge0 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 1st ‘ 𝑎 ) ∈ 𝑋 ∧ ( 2nd ‘ 𝑎 ) ∈ 𝑋 ) → 0 ≤ ( ( 1st ‘ 𝑎 ) 𝐷 ( 2nd ‘ 𝑎 ) ) )
7 6 3expb ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( ( 1st ‘ 𝑎 ) ∈ 𝑋 ∧ ( 2nd ‘ 𝑎 ) ∈ 𝑋 ) ) → 0 ≤ ( ( 1st ‘ 𝑎 ) 𝐷 ( 2nd ‘ 𝑎 ) ) )
8 5 7 sylan2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ( 𝑋 × 𝑋 ) ) → 0 ≤ ( ( 1st ‘ 𝑎 ) 𝐷 ( 2nd ‘ 𝑎 ) ) )
9 1st2nd2 ⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) → 𝑎 = ⟨ ( 1st ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ )
10 9 fveq2d ⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ ⟨ ( 1st ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ ) )
11 df-ov ⊢ ( ( 1st ‘ 𝑎 ) 𝐷 ( 2nd ‘ 𝑎 ) ) = ( 𝐷 ‘ ⟨ ( 1st ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ )
12 10 11 eqtr4di ⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) → ( 𝐷 ‘ 𝑎 ) = ( ( 1st ‘ 𝑎 ) 𝐷 ( 2nd ‘ 𝑎 ) ) )
13 12 adantl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝐷 ‘ 𝑎 ) = ( ( 1st ‘ 𝑎 ) 𝐷 ( 2nd ‘ 𝑎 ) ) )
14 8 13 breqtrrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ( 𝑋 × 𝑋 ) ) → 0 ≤ ( 𝐷 ‘ 𝑎 ) )
15 elxrge0 ⊢ ( ( 𝐷 ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐷 ‘ 𝑎 ) ∈ ℝ* ∧ 0 ≤ ( 𝐷 ‘ 𝑎 ) ) )
16 3 14 15 sylanbrc ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝐷 ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
17 16 ralrimiva ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑎 ∈ ( 𝑋 × 𝑋 ) ( 𝐷 ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
18 fnfvrnss ⊢ ( ( 𝐷 Fn ( 𝑋 × 𝑋 ) ∧ ∀ 𝑎 ∈ ( 𝑋 × 𝑋 ) ( 𝐷 ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) ) → ran 𝐷 ⊆ ( 0 [,] +∞ ) )
19 2 17 18 syl2anc ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ran 𝐷 ⊆ ( 0 [,] +∞ ) )
20 df-f ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) ↔ ( 𝐷 Fn ( 𝑋 × 𝑋 ) ∧ ran 𝐷 ⊆ ( 0 [,] +∞ ) ) )
21 2 19 20 sylanbrc ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) )