Metamath Proof Explorer


Theorem blrnps

Description: Membership in the range of the ball function. Note that ran ( ballD ) is the collection of all balls for metric D . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blrnps D PsMet X A ran ball D x X r * A = x ball D r

Proof

Step Hyp Ref Expression
1 blfps D PsMet X ball D : X × * 𝒫 X
2 ffn ball D : X × * 𝒫 X ball D Fn X × *
3 ovelrn ball D Fn X × * A ran ball D x X r * A = x ball D r
4 1 2 3 3syl D PsMet X A ran ball D x X r * A = x ball D r