Metamath Proof Explorer


Theorem blfval

Description: The value of the ball function. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 11-Nov-2013) (Proof shortened by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion blfval D ∞Met X ball D = x X , r * y X | x D y < r

Proof

Step Hyp Ref Expression
1 xmetpsmet D ∞Met X D PsMet X
2 blfvalps D PsMet X ball D = x X , r * y X | x D y < r
3 1 2 syl D ∞Met X ball D = x X , r * y X | x D y < r