Metamath Proof Explorer

Theorem metcl

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

Proof

Step Hyp Ref Expression
1 metf 
 |-  ( 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 )