Metamath Proof Explorer

Theorem psmetcl

Description: Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmetcl 
|- ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )

Proof

Step Hyp Ref Expression
1 psmetf 
 |-  ( D e. ( PsMet ` 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. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )