Metamath Proof Explorer

Theorem xmetcl

Description: Closure of the distance function of a metric space. Part of Property M1 of Kreyszig p. 3. (Contributed by NM, 30-Aug-2006)

Ref Expression
Assertion xmetcl ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 𝐷 𝐡 ) ∈ ℝ* )

Proof

Step Hyp Ref Expression
1 xmetf ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐷 : ( 𝑋 Γ— 𝑋 ) ⟢ ℝ* )
2 fovcdm ⊒ ( ( 𝐷 : ( 𝑋 Γ— 𝑋 ) ⟢ ℝ* ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 𝐷 𝐡 ) ∈ ℝ* )
3 1 2 syl3an1 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) β†’ ( 𝐴 𝐷 𝐡 ) ∈ ℝ* )