Definition df-bl 18965

Description: Define the metric space ball function. See blval 21401 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 18957	. 2 class ball
2		vd	. . 3 setvar d
3		cvv 3045	. . 3 class _V
4		vx	. . . 4 setvar x
5		vz	. . . 4 setvar z
6	2	cv 1443	. . . . . 6 class d
7	6	cdm 4834	. . . . 5 class dom d
8	7	cdm 4834	. . . 4 class dom dom d
9		cxr 9674	. . . 4 class RR*
10	4	cv 1443	. . . . . . 7 class x
11		vy	. . . . . . . 8 setvar y
12	11	cv 1443	. . . . . . 7 class y
13	10, 12, 6	co 6290	. . . . . 6 class ( x d y )
14	5	cv 1443	. . . . . 6 class z
15		clt 9675	. . . . . 6 class <
16	13, 14, 15	wbr 4402	. . . . 5 wff ( x d y ) < z
17	16, 11, 8	crab 2741	. . . 4 class { y e. dom dom d | ( x d y ) < z }
18	4, 5, 8, 9, 17	cmpt2 6292	. . 3 class ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } )
19	2, 3, 18	cmpt 4461	. 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 1444	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  21398