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	⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) ↔ ( 𝑎 = ⟨ ( 1^st ‘ 𝑎 ) , ( 2^nd ‘ 𝑎 ) ⟩ ∧ ( ( 1^st ‘ 𝑎 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝑋 ) ) )
5	4	simprbi	⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) → ( ( 1^st ‘ 𝑎 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝑋 ) )
6		psmetge0	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 1^st ‘ 𝑎 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝑋 ) → 0 ≤ ( ( 1^st ‘ 𝑎 ) 𝐷 ( 2^nd ‘ 𝑎 ) ) )
7	6	3expb	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( ( 1^st ‘ 𝑎 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝑎 ) ∈ 𝑋 ) ) → 0 ≤ ( ( 1^st ‘ 𝑎 ) 𝐷 ( 2^nd ‘ 𝑎 ) ) )
8	5 7	sylan2	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ( 𝑋 × 𝑋 ) ) → 0 ≤ ( ( 1^st ‘ 𝑎 ) 𝐷 ( 2^nd ‘ 𝑎 ) ) )
9		1st2nd2	⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) → 𝑎 = ⟨ ( 1^st ‘ 𝑎 ) , ( 2^nd ‘ 𝑎 ) ⟩ )
10	9	fveq2d	⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ ⟨ ( 1^st ‘ 𝑎 ) , ( 2^nd ‘ 𝑎 ) ⟩ ) )
11		df-ov	⊢ ( ( 1^st ‘ 𝑎 ) 𝐷 ( 2^nd ‘ 𝑎 ) ) = ( 𝐷 ‘ ⟨ ( 1^st ‘ 𝑎 ) , ( 2^nd ‘ 𝑎 ) ⟩ )
12	10 11	eqtr4di	⊢ ( 𝑎 ∈ ( 𝑋 × 𝑋 ) → ( 𝐷 ‘ 𝑎 ) = ( ( 1^st ‘ 𝑎 ) 𝐷 ( 2^nd ‘ 𝑎 ) ) )
13	12	adantl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑎 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝐷 ‘ 𝑎 ) = ( ( 1^st ‘ 𝑎 ) 𝐷 ( 2^nd ‘ 𝑎 ) ) )
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 [,] +∞ ) )

Metamath Proof Explorer

Theorem psmetxrge0

Proof