Definition df-bl 20505

Description: Define the metric space ball function. See blval 23447 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 20497	. 2 class ball
2		vd	. . 3 setvar 𝑑
3		cvv 3422	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vz	. . . 4 setvar 𝑧
6	2	cv 1538	. . . . . 6 class 𝑑
7	6	cdm 5580	. . . . 5 class dom 𝑑
8	7	cdm 5580	. . . 4 class dom dom 𝑑
9		cxr 10939	. . . 4 class ℝ*
10	4	cv 1538	. . . . . . 7 class 𝑥
11		vy	. . . . . . . 8 setvar 𝑦
12	11	cv 1538	. . . . . . 7 class 𝑦
13	10, 12, 6	co 7255	. . . . . 6 class (𝑥𝑑𝑦)
14	5	cv 1538	. . . . . 6 class 𝑧
15		clt 10940	. . . . . 6 class <
16	13, 14, 15	wbr 5070	. . . . 5 wff (𝑥𝑑𝑦) < 𝑧
17	16, 11, 8	crab 3067	. . . 4 class {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}
18	4, 5, 8, 9, 17	cmpo 7257	. . 3 class (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧})
19	2, 3, 18	cmpt 5153	. 2 class (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))
20	1, 19	wceq 1539	1 wff ball = (𝑑 ∈ V ↦ (𝑥 ∈ dom dom 𝑑, 𝑧 ∈ ℝ* ↦ {𝑦 ∈ dom dom 𝑑 ∣ (𝑥𝑑𝑦) < 𝑧}))

This definition is referenced by:  blfvalps  23444