Definition df-bl 14102

Description: Define the metric space ball function. (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 14094	. 2 class ball
2		vd	. . 3 setvar 𝑑
3		cvv 2763	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vz	. . . 4 setvar 𝑧
6	2	cv 1363	. . . . . 6 class 𝑑
7	6	cdm 4663	. . . . 5 class dom 𝑑
8	7	cdm 4663	. . . 4 class dom dom 𝑑
9		cxr 8060	. . . 4 class ℝ*
10	4	cv 1363	. . . . . . 7 class 𝑥
11		vy	. . . . . . . 8 setvar 𝑦
12	11	cv 1363	. . . . . . 7 class 𝑦
13	10, 12, 6	co 5922	. . . . . 6 class (𝑥𝑑𝑦)
14	5	cv 1363	. . . . . 6 class 𝑧
15		clt 8061	. . . . . 6 class <
16	13, 14, 15	wbr 4033	. . . . 5 wff (𝑥𝑑𝑦) < 𝑧
17	16, 11, 8	crab 2479	. . . 4 class {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}
18	4, 5, 8, 9, 17	cmpo 5924	. . 3 class (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧})
19	2, 3, 18	cmpt 4094	. 2 class (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
20	1, 19	wceq 1364	1 wff ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))

This definition is referenced by:  blfn  14107  blfvalps  14621