Definition df-bl

Description: Define the metric space ball function. See blval for its value. (Contributed by NM, 30-Aug-2006) (Revised by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Assertion	df-bl	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbl	|- ball
1		vd	|- d
2		cvv	|- _V
3		vx	|- x
4	1	cv	|- d
5	4	cdm	|- dom d
6	5	cdm	|- dom dom d
7		vz	|- z
8		cxr	|- RR*
9		vy	|- y
10	3	cv	|- x
11	9	cv	|- y
12	10 11 4	co	|- ( x d y )
13		clt	|- <
14	7	cv	|- z
15	12 14 13	wbr	|- ( x d y ) < z
16	15 9 6	crab	|- { y e. dom dom d | ( x d y ) < z }
17	3 7 6 8 16	cmpo	|- ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } )
18	1 2 17	cmpt	|- ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
19	0 18	wceq	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )