Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-psmet Unicode version

Definition df-psmet 12215
 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
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-psmet
StepHypRef Expression
1 cpsmet 12207 . 2 PsMet
2 vx . . 3
3 cvv 2690 . . 3
4 vy . . . . . . . . 9
54cv 1331 . . . . . . . 8
6 vd . . . . . . . . 9
76cv 1331 . . . . . . . 8
85, 5, 7co 5783 . . . . . . 7
9 cc0 7664 . . . . . . 7
108, 9wceq 1332 . . . . . 6
11 vz . . . . . . . . . . 11
1211cv 1331 . . . . . . . . . 10
135, 12, 7co 5783 . . . . . . . . 9
14 vw . . . . . . . . . . . 12
1514cv 1331 . . . . . . . . . . 11
1615, 5, 7co 5783 . . . . . . . . . 10
1715, 12, 7co 5783 . . . . . . . . . 10
18 cxad 9607 . . . . . . . . . 10
1916, 17, 18co 5783 . . . . . . . . 9
20 cle 7845 . . . . . . . . 9
2113, 19, 20wbr 3938 . . . . . . . 8
222cv 1331 . . . . . . . 8
2321, 14, 22wral 2417 . . . . . . 7
2423, 11, 22wral 2417 . . . . . 6
2510, 24wa 103 . . . . 5
2625, 4, 22wral 2417 . . . 4
27 cxr 7843 . . . . 5
2822, 22cxp 4546 . . . . 5
29 cmap 6551 . . . . 5
3027, 28, 29co 5783 . . . 4
3126, 6, 30crab 2421 . . 3
322, 3, 31cmpt 3998 . 2
331, 32wceq 1332 1 PsMet
 Colors of variables: wff set class This definition is referenced by:  psmetrel  12550  ispsmet  12551  psmetdmdm  12552  psmetf  12553  psmet0  12555  psmettri2  12556  psmetres2  12561
 Copyright terms: Public domain W3C validator