Definition df-psmet 14099

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 14091	. 2 class PsMet
2		vx	. . 3 setvar x
3		cvv 2763	. . 3 class _V
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1363	. . . . . . . 8 class y
6		vd	. . . . . . . . 9 setvar d
7	6	cv 1363	. . . . . . . 8 class d
8	5, 5, 7	co 5922	. . . . . . 7 class ( y d y )
9		cc0 7879	. . . . . . 7 class 0
10	8, 9	wceq 1364	. . . . . 6 wff ( y d y ) = 0
11		vz	. . . . . . . . . . 11 setvar z
12	11	cv 1363	. . . . . . . . . 10 class z
13	5, 12, 7	co 5922	. . . . . . . . 9 class ( y d z )
14		vw	. . . . . . . . . . . 12 setvar w
15	14	cv 1363	. . . . . . . . . . 11 class w
16	15, 5, 7	co 5922	. . . . . . . . . 10 class ( w d y )
17	15, 12, 7	co 5922	. . . . . . . . . 10 class ( w d z )
18		cxad 9845	. . . . . . . . . 10 class +e
19	16, 17, 18	co 5922	. . . . . . . . 9 class ( ( w d y ) +e ( w d z ) )
20		cle 8062	. . . . . . . . 9 class <_
21	13, 19, 20	wbr 4033	. . . . . . . 8 wff ( y d z ) <_ ( ( w d y ) +e ( w d z ) )
22	2	cv 1363	. . . . . . . 8 class x
23	21, 14, 22	wral 2475	. . . . . . 7 wff A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) )
24	23, 11, 22	wral 2475	. . . . . 6 wff A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) )
25	10, 24	wa 104	. . . . 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 2475	. . . 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 8060	. . . . 5 class RR*
28	22, 22	cxp 4661	. . . . 5 class ( x X. x )
29		cmap 6707	. . . . 5 class ^m
30	27, 28, 29	co 5922	. . . 4 class ( RR* ^m ( x X. x ) )
31	26, 6, 30	crab 2479	. . 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 4094	. 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 1364	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  14558  ispsmet  14559  psmetdmdm  14560  psmetf  14561  psmet0  14563  psmettri2  14564  psmetres2  14569