Definition df-bl 16652

Description: Define the metric space ball function. See blval 18369 for its value. (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 16643	. 2 class ball
2		vd	. . 3 set d
3		cvv 2916	. . 3 class _V
4		vx	. . . 4 set x
5		vz	. . . 4 set z
6	2	cv 1648	. . . . . 6 class d
7	6	cdm 4837	. . . . 5 class dom d
8	7	cdm 4837	. . . 4 class dom dom d
9		cxr 9075	. . . 4 class RR*
10	4	cv 1648	. . . . . . 7 class x
11		vy	. . . . . . . 8 set y
12	11	cv 1648	. . . . . . 7 class y
13	10, 12, 6	co 6040	. . . . . 6 class ( x d y )
14	5	cv 1648	. . . . . 6 class z
15		clt 9076	. . . . . 6 class <
16	13, 14, 15	wbr 4172	. . . . 5 wff ( x d y ) < z
17	16, 11, 8	crab 2670	. . . 4 class { y e. dom dom d | ( x d y ) < z }
18	4, 5, 8, 9, 17	cmpt2 6042	. . 3 class ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } )
19	2, 3, 18	cmpt 4226	. 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 1649	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:  blfvalps  18366