Definition df-psmet 12781

Description: Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)

Assertion

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

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

Detailed syntax breakdown of Definition df-psmet

Step	Hyp	Ref	Expression
1		cpsmet 12773	. 2 class PsMet
2		vx	. . 3 setvar x
3		cvv 2730	. . 3 class _V
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1347	. . . . . . . 8 class y
6		vd	. . . . . . . . 9 setvar d
7	6	cv 1347	. . . . . . . 8 class d
8	5, 5, 7	co 5853	. . . . . . 7 class ( y d y )
9		cc0 7774	. . . . . . 7 class 0
10	8, 9	wceq 1348	. . . . . 6 wff ( y d y ) = 0
11		vz	. . . . . . . . . . 11 setvar z
12	11	cv 1347	. . . . . . . . . 10 class z
13	5, 12, 7	co 5853	. . . . . . . . 9 class ( y d z )
14		vw	. . . . . . . . . . . 12 setvar w
15	14	cv 1347	. . . . . . . . . . 11 class w
16	15, 5, 7	co 5853	. . . . . . . . . 10 class ( w d y )
17	15, 12, 7	co 5853	. . . . . . . . . 10 class ( w d z )
18		cxad 9727	. . . . . . . . . 10 class +e
19	16, 17, 18	co 5853	. . . . . . . . 9 class ( ( w d y ) +e ( w d z ) )
20		cle 7955	. . . . . . . . 9 class <_
21	13, 19, 20	wbr 3989	. . . . . . . 8 wff ( y d z ) <_ ( ( w d y ) +e ( w d z ) )
22	2	cv 1347	. . . . . . . 8 class x
23	21, 14, 22	wral 2448	. . . . . . 7 wff A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) )
24	23, 11, 22	wral 2448	. . . . . 6 wff A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) )
25	10, 24	wa 103	. . . . 5 wff ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) )
26	25, 4, 22	wral 2448	. . . 4 wff A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) )
27		cxr 7953	. . . . 5 class RR*
28	22, 22	cxp 4609	. . . . 5 class ( x X. x )
29		cmap 6626	. . . . 5 class ^m
30	27, 28, 29	co 5853	. . . 4 class ( RR* ^m ( x X. x ) )
31	26, 6, 30	crab 2452	. . 3 class { d e. ( RR* ^m ( x X. x ) ) | A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) }
32	2, 3, 31	cmpt 4050	. 2 class ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
33	1, 32	wceq 1348	1 wff PsMet = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )

This definition is referenced by:  psmetrel  13116  ispsmet  13117  psmetdmdm  13118  psmetf  13119  psmet0  13121  psmettri2  13122  psmetres2  13127