df-psmet

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)

		Ref	Expression
	Assertion	df-psmet	$⊢ PsMet = (x \in V ⟼ \{d \in ({ℝ^{*}}^{(x \times x)}) \| \forall y \in x (y d y = 0 \land \forall z \in x \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpsmet	$class PsMet$
1		vx	$setvar x$
2		cvv	$class V$
3		vd	$setvar d$
4		cxr	$class ℝ^{*}$
5		cmap	$class ↑_{𝑚}$
6	1	cv	$setvar x$
7	6 6	cxp	$class (x \times x)$
8	4 7 5	co	$class ({ℝ^{*}}^{(x \times x)})$
9		vy	$setvar y$
10	9	cv	$setvar y$
11	3	cv	$setvar d$
12	10 10 11	co	$class (y d y)$
13		cc0	$class 0$
14	12 13	wceq	$wff y d y = 0$
15		vz	$setvar z$
16		vw	$setvar w$
17	15	cv	$setvar z$
18	10 17 11	co	$class (y d z)$
19		cle	$class \leq$
20	16	cv	$setvar w$
21	20 10 11	co	$class (w d y)$
22		cxad	$class +_{𝑒}$
23	20 17 11	co	$class (w d z)$
24	21 23 22	co	$class ((w d y) +_{𝑒} (w d z))$
25	18 24 19	wbr	$wff y d z \leq (w d y) +_{𝑒} (w d z)$
26	25 16 6	wral	$wff \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z)$
27	26 15 6	wral	$wff \forall z \in x \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z)$
28	14 27	wa	$wff (y d y = 0 \land \forall z \in x \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))$
29	28 9 6	wral	$wff \forall y \in x (y d y = 0 \land \forall z \in x \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))$
30	29 3 8	crab	$class \{d \in ({ℝ^{*}}^{(x \times x)}) \| \forall y \in x (y d y = 0 \land \forall z \in x \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))\}$
31	1 2 30	cmpt	$class (x \in V ⟼ \{d \in ({ℝ^{*}}^{(x \times x)}) \| \forall y \in x (y d y = 0 \land \forall z \in x \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))\})$
32	0 31	wceq	$wff PsMet = (x \in V ⟼ \{d \in ({ℝ^{*}}^{(x \times x)}) \| \forall y \in x (y d y = 0 \land \forall z \in x \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))\})$

Metamath Proof Explorer

Definition df-psmet

Detailed syntax breakdown