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 e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )

Proof

Step Hyp Ref Expression
1 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
2 fovrn 
 |-  ( ( D : ( X X. X ) --> RR* /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
3 1 2 syl3an1 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )