Definition df-met 9936

Description: Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 9937. However, we will often also call the metric itself a "metric space.") Equivalent to Definition 14-1.1 of [Gleason] p. 223. See ismsg 9943 for the property "is a metric space." The 4 properties in Gleason's definition are shown by met0 9958, metgt0 9963, metsym 9959, and mettri 9960.

Assertion

Ref	Expression
df-met	|- Met = {x | E.y(x:(y X. y)-->RR /\ A.z e. y A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw))))}

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

Detailed syntax breakdown of Definition df-met

Step	Hyp	Ref	Expression
1		cme 9932	. 2 class Met
2		vy	. . . . . . . 8 set y
3	2	cv 1585	. . . . . . 7 class y
4	3, 3	cxp 4117	. . . . . 6 class (y X. y)
5		cr 6751	. . . . . 6 class RR
6		vx	. . . . . . 7 set x
7	6	cv 1585	. . . . . 6 class x
8	4, 5, 7	wf 4127	. . . . 5 wff x:(y X. y)-->RR
9		vz	. . . . . . . . . . . 12 set z
10	9	cv 1585	. . . . . . . . . . 11 class z
11		vw	. . . . . . . . . . . 12 set w
12	11	cv 1585	. . . . . . . . . . 11 class w
13	10, 12, 7	co 4981	. . . . . . . . . 10 class (zxw)
14		cc0 6752	. . . . . . . . . 10 class 0
15	13, 14	wceq 1586	. . . . . . . . 9 wff (zxw) = 0
16	10, 12	wceq 1586	. . . . . . . . 9 wff z = w
17	15, 16	wb 219	. . . . . . . 8 wff ((zxw) = 0 <-> z = w)
18		vv	. . . . . . . . . . . . 13 set v
19	18	cv 1585	. . . . . . . . . . . 12 class v
20	19, 10, 7	co 4981	. . . . . . . . . . 11 class (vxz)
21	19, 12, 7	co 4981	. . . . . . . . . . 11 class (vxw)
22		caddc 6755	. . . . . . . . . . 11 class +
23	20, 21, 22	co 4981	. . . . . . . . . 10 class ((vxz) + (vxw))
24		cle 6841	. . . . . . . . . 10 class <_
25	13, 23, 24	wbr 3507	. . . . . . . . 9 wff (zxw) <_ ((vxz) + (vxw))
26	25, 18, 3	wral 2355	. . . . . . . 8 wff A.v e. y (zxw) <_ ((vxz) + (vxw))
27	17, 26	wa 337	. . . . . . 7 wff (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw)))
28	27, 11, 3	wral 2355	. . . . . 6 wff A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw)))
29	28, 9, 3	wral 2355	. . . . 5 wff A.z e. y A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw)))
30	8, 29	wa 337	. . . 4 wff (x:(y X. y)-->RR /\ A.z e. y A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw))))
31	30, 2	wex 1615	. . 3 wff E.y(x:(y X. y)-->RR /\ A.z e. y A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw))))
32	31, 6	cab 2128	. 2 class {x | E.y(x:(y X. y)-->RR /\ A.z e. y A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw))))}
33	1, 32	wceq 1586	1 wff Met = {x | E.y(x:(y X. y)-->RR /\ A.z e. y A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw))))}

This definition is referenced by:  ismet 9941

Copyright terms: Public domain