Definition df-bl 17656

Description: Define the metric space ball function. See blval 19803 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 17647	. 2 class ball
2		vd	. . 3 setvar d
3		cvv 2962	. . 3 class _V
4		vx	. . . 4 setvar x
5		vz	. . . 4 setvar z
6	2	cv 1361	. . . . . 6 class d
7	6	cdm 4827	. . . . 5 class dom d
8	7	cdm 4827	. . . 4 class dom dom d
9		cxr 9405	. . . 4 class RR*
10	4	cv 1361	. . . . . . 7 class x
11		vy	. . . . . . . 8 setvar y
12	11	cv 1361	. . . . . . 7 class y
13	10, 12, 6	co 6080	. . . . . 6 class ( x d y )
14	5	cv 1361	. . . . . 6 class z
15		clt 9406	. . . . . 6 class <
16	13, 14, 15	wbr 4280	. . . . 5 wff ( x d y ) < z
17	16, 11, 8	crab 2709	. . . 4 class { y e. dom dom d | ( x d y ) < z }
18	4, 5, 8, 9, 17	cmpt2 6082	. . 3 class ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } )
19	2, 3, 18	cmpt 4338	. 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 1362	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  19800