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 ⊢ D ∈ PsMet ⁡ X → D : X × X ⟶ 0 +∞

Proof

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