Definition df-bl 9072

Description: Define the metric space ball function. See blval 9114 for its value.

Assertion

Ref	Expression
df-bl	|- ball = {<.x, y>. | (x e. Met /\ y = {<.<.z, w>., v>. | ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))})}

Distinct variable group:   x,y,z,w,v,u

Detailed syntax breakdown of Definition df-bl

Step	Hyp	Ref	Expression
1		cbl 9068	. 2 class ball
2		vx	. . . . . 6 set x
3	2	cv 1297	. . . . 5 class x
4		cme 9066	. . . . 5 class Met
5	3, 4	wcel 1300	. . . 4 wff x e. Met
6		vy	. . . . . 6 set y
7	6	cv 1297	. . . . 5 class y
8		vz	. . . . . . . . . 10 set z
9	8	cv 1297	. . . . . . . . 9 class z
10	3	cdm 3986	. . . . . . . . . 10 class dom x
11	10	cdm 3986	. . . . . . . . 9 class dom dom x
12	9, 11	wcel 1300	. . . . . . . 8 wff z e. dom dom x
13		vw	. . . . . . . . . 10 set w
14	13	cv 1297	. . . . . . . . 9 class w
15		cr 6385	. . . . . . . . 9 class RR
16	14, 15	wcel 1300	. . . . . . . 8 wff w e. RR
17	12, 16	wa 240	. . . . . . 7 wff (z e. dom dom x /\ w e. RR)
18		cc0 6386	. . . . . . . . 9 class 0
19		clt 6653	. . . . . . . . 9 class <
20	18, 14, 19	wbr 3338	. . . . . . . 8 wff 0 < w
21		vv	. . . . . . . . . 10 set v
22	21	cv 1297	. . . . . . . . 9 class v
23		vu	. . . . . . . . . . . . 13 set u
24	23	cv 1297	. . . . . . . . . . . 12 class u
25	9, 24, 3	co 4884	. . . . . . . . . . 11 class (zxu)
26	25, 14, 19	wbr 3338	. . . . . . . . . 10 wff (zxu) < w
27	26, 23, 11	crab 2108	. . . . . . . . 9 class {u e. dom dom x | (zxu) < w}
28	22, 27	wceq 1298	. . . . . . . 8 wff v = {u e. dom dom x | (zxu) < w}
29	20, 28	wa 240	. . . . . . 7 wff (0 < w /\ v = {u e. dom dom x | (zxu) < w})
30	17, 29	wa 240	. . . . . 6 wff ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))
31	30, 8, 13, 21	copab2 4885	. . . . 5 class {<.<.z, w>., v>. | ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))}
32	7, 31	wceq 1298	. . . 4 wff y = {<.<.z, w>., v>. | ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))}
33	5, 32	wa 240	. . 3 wff (x e. Met /\ y = {<.<.z, w>., v>. | ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))})
34	33, 2, 6	copab 3395	. 2 class {<.x, y>. | (x e. Met /\ y = {<.<.z, w>., v>. | ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))})}
35	1, 34	wceq 1298	1 wff ball = {<.x, y>. | (x e. Met /\ y = {<.<.z, w>., v>. | ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))})}

This definition is referenced by:  blfval 9112

Copyright terms: Public domain