Definition df-bl 14178

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 = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )

Distinct variable group:   x, d, y, z

Detailed syntax breakdown of Definition df-bl

Step	Hyp	Ref	Expression
1		cbl 14170	. 2 class ball
2		vd	. . 3 setvar d
3		cvv 2763	. . 3 class _V
4		vx	. . . 4 setvar x
5		vz	. . . 4 setvar z
6	2	cv 1363	. . . . . 6 class d
7	6	cdm 4664	. . . . 5 class dom d
8	7	cdm 4664	. . . 4 class dom dom d
9		cxr 8077	. . . 4 class RR*
10	4	cv 1363	. . . . . . 7 class x
11		vy	. . . . . . . 8 setvar y
12	11	cv 1363	. . . . . . 7 class y
13	10, 12, 6	co 5925	. . . . . 6 class ( x d y )
14	5	cv 1363	. . . . . 6 class z
15		clt 8078	. . . . . 6 class <
16	13, 14, 15	wbr 4034	. . . . 5 wff ( x d y ) < z
17	16, 11, 8	crab 2479	. . . 4 class { y e. dom dom d | ( x d y ) < z }
18	4, 5, 8, 9, 17	cmpo 5927	. . 3 class ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } )
19	2, 3, 18	cmpt 4095	. 2 class ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
20	1, 19	wceq 1364	1 wff ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )

This definition is referenced by:  blfn  14183  blfvalps  14705