Theorem blval

Description: The ball around a point P is the set of all points whose distance from P is less than the ball's radius R . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Assertion	blval	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )

Proof

Step	Hyp	Ref	Expression
1		blfval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑦 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑥 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑥 ) < 𝑟 } ) )
2	1	3ad2ant1	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( ball ‘ 𝐷 ) = ( 𝑦 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑥 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑥 ) < 𝑟 } ) )
3		simprl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃 ∧ 𝑟 = 𝑅 ) ) → 𝑦 = 𝑃 )
4	3	oveq1d	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃 ∧ 𝑟 = 𝑅 ) ) → ( 𝑦 𝐷 𝑥 ) = ( 𝑃 𝐷 𝑥 ) )
5		simprr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃 ∧ 𝑟 = 𝑅 ) ) → 𝑟 = 𝑅 )
6	4 5	breq12d	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃 ∧ 𝑟 = 𝑅 ) ) → ( ( 𝑦 𝐷 𝑥 ) < 𝑟 ↔ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
7	6	rabbidv	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃 ∧ 𝑟 = 𝑅 ) ) → { 𝑥 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑥 ) < 𝑟 } = { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )
8		simp2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝑃 ∈ 𝑋 )
9		simp3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝑅 ∈ ℝ* )
10		elfvdm	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
11	10	3ad2ant1	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → 𝑋 ∈ dom ∞Met )
12		rabexg	⊢ ( 𝑋 ∈ dom ∞Met → { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } ∈ V )
13	11 12	syl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } ∈ V )
14	2 7 8 9 13	ovmpod	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )