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\in \mathrm{\infty Met}\left(X\right)\to \mathrm{ball}\left(D\right)=\left(x\in X,r\in {ℝ}^{*}⟼\left\{y\in X|xDy<r\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		xmetpsmet	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D\in \mathrm{PsMet}\left(X\right)$$
2		blfvalps	$$⊢D\in \mathrm{PsMet}\left(X\right)\to \mathrm{ball}\left(D\right)=\left(x\in X,r\in {ℝ}^{*}⟼\left\{y\in X|xDy<r\right\}\right)$$
3	1 2	syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{ball}\left(D\right)=\left(x\in X,r\in {ℝ}^{*}⟼\left\{y\in X|xDy<r\right\}\right)$$