Definition df-bl

Description: Define the metric space ball function. See blval for its value. (Contributed by NM, 30-Aug-2006) (Revised by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Assertion	df-bl	⊢ ball = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ dom dom 𝑑 , 𝑧 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbl	⊢ ball
1		vd	⊢ 𝑑
2		cvv	⊢ V
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑑
5	4	cdm	⊢ dom 𝑑
6	5	cdm	⊢ dom dom 𝑑
7		vz	⊢ 𝑧
8		cxr	⊢ ℝ*
9		vy	⊢ 𝑦
10	3	cv	⊢ 𝑥
11	9	cv	⊢ 𝑦
12	10 11 4	co	⊢ ( 𝑥 𝑑 𝑦 )
13		clt	⊢ <
14	7	cv	⊢ 𝑧
15	12 14 13	wbr	⊢ ( 𝑥 𝑑 𝑦 ) < 𝑧
16	15 9 6	crab	⊢ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 }
17	3 7 6 8 16	cmpo	⊢ ( 𝑥 ∈ dom dom 𝑑 , 𝑧 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 } )
18	1 2 17	cmpt	⊢ ( 𝑑 ∈ V ↦ ( 𝑥 ∈ dom dom 𝑑 , 𝑧 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 } ) )
19	0 18	wceq	⊢ ball = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ dom dom 𝑑 , 𝑧 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 } ) )