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	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )

Proof

Step	Hyp	Ref	Expression
1		xmetpsmet	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2		blfvalps	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )
3	1 2	syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )