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 D ∞Met X A X B X A D B *


Step Hyp Ref Expression
1 xmetf D ∞Met X D : X × X *
2 fovrn D : X × X * A X B X A D B *
3 1 2 syl3an1 D ∞Met X A X B X A D B *