Definition df-met 19740

Description: Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 22126. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. The 4 properties in Gleason's definition are shown by met0 22148, metgt0 22164, metsym 22155, and mettri 22157. (Contributed by NM, 25-Aug-2006.)

Assertion

Ref	Expression
df-met	|- Met = ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )

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

Detailed syntax breakdown of Definition df-met

Step	Hyp	Ref	Expression
1		cme 19732	. 2 class Met
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vy	. . . . . . . . . . 11 setvar y
5	4	cv 1482	. . . . . . . . . 10 class y
6		vz	. . . . . . . . . . 11 setvar z
7	6	cv 1482	. . . . . . . . . 10 class z
8		vd	. . . . . . . . . . 11 setvar d
9	8	cv 1482	. . . . . . . . . 10 class d
10	5, 7, 9	co 6650	. . . . . . . . 9 class ( y d z )
11		cc0 9936	. . . . . . . . 9 class 0
12	10, 11	wceq 1483	. . . . . . . 8 wff ( y d z ) = 0
13	4, 6	weq 1874	. . . . . . . 8 wff y = z
14	12, 13	wb 196	. . . . . . 7 wff ( ( y d z ) = 0 <-> y = z )
15		vw	. . . . . . . . . . . 12 setvar w
16	15	cv 1482	. . . . . . . . . . 11 class w
17	16, 5, 9	co 6650	. . . . . . . . . 10 class ( w d y )
18	16, 7, 9	co 6650	. . . . . . . . . 10 class ( w d z )
19		caddc 9939	. . . . . . . . . 10 class +
20	17, 18, 19	co 6650	. . . . . . . . 9 class ( ( w d y ) + ( w d z ) )
21		cle 10075	. . . . . . . . 9 class <_
22	10, 20, 21	wbr 4653	. . . . . . . 8 wff ( y d z ) <_ ( ( w d y ) + ( w d z ) )
23	2	cv 1482	. . . . . . . 8 class x
24	22, 15, 23	wral 2912	. . . . . . 7 wff A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) )
25	14, 24	wa 384	. . . . . 6 wff ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) )
26	25, 6, 23	wral 2912	. . . . 5 wff A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) )
27	26, 4, 23	wral 2912	. . . 4 wff A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) )
28		cr 9935	. . . . 5 class RR
29	23, 23	cxp 5112	. . . . 5 class ( x X. x )
30		cmap 7857	. . . . 5 class ^m
31	28, 29, 30	co 6650	. . . 4 class ( RR ^m ( x X. x ) )
32	27, 8, 31	crab 2916	. . 3 class { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) }
33	2, 3, 32	cmpt 4729	. 2 class ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )
34	1, 33	wceq 1483	1 wff Met = ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )

This definition is referenced by:  ismet  22128