Definition df-bl 19562

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

Assertion

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

Distinct variable group:   𝑥,𝑑,𝑦,𝑧

Detailed syntax breakdown of Definition df-bl

Step	Hyp	Ref	Expression
1		cbl 19554	. 2 class ball
2		vd	. . 3 setvar 𝑑
3		cvv 3173	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vz	. . . 4 setvar 𝑧
6	2	cv 1474	. . . . . 6 class 𝑑
7	6	cdm 5038	. . . . 5 class dom 𝑑
8	7	cdm 5038	. . . 4 class dom dom 𝑑
9		cxr 9952	. . . 4 class ℝ*
10	4	cv 1474	. . . . . . 7 class 𝑥
11		vy	. . . . . . . 8 setvar 𝑦
12	11	cv 1474	. . . . . . 7 class 𝑦
13	10, 12, 6	co 6549	. . . . . 6 class (𝑥𝑑𝑦)
14	5	cv 1474	. . . . . 6 class 𝑧
15		clt 9953	. . . . . 6 class <
16	13, 14, 15	wbr 4583	. . . . 5 wff (𝑥𝑑𝑦) < 𝑧
17	16, 11, 8	crab 2900	. . . 4 class {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}
18	4, 5, 8, 9, 17	cmpt2 6551	. . 3 class (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧})
19	2, 3, 18	cmpt 4643	. 2 class (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
20	1, 19	wceq 1475	1 wff ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))

This definition is referenced by:  blfvalps  21998