Metamath Proof Explorer

Definition 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 ∈ V ⟼ d ∈ ℝ * x × x | ∀ y ∈ x y d y = 0 ∧ ∀ z ∈ x ∀ w ∈ x y d z ≤ 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 × x
8 4 7 5 co class ℝ * x × 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 ≤
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 ≤ w d y + 𝑒 w d z
26 25 16 6 wral wff ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
27 26 15 6 wral wff ∀ z ∈ x ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
28 14 27 wa wff y d y = 0 ∧ ∀ z ∈ x ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
29 28 9 6 wral wff ∀ y ∈ x y d y = 0 ∧ ∀ z ∈ x ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
30 29 3 8 crab class d ∈ ℝ * x × x | ∀ y ∈ x y d y = 0 ∧ ∀ z ∈ x ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
31 1 2 30 cmpt class x ∈ V ⟼ d ∈ ℝ * x × x | ∀ y ∈ x y d y = 0 ∧ ∀ z ∈ x ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
32 0 31 wceq wff PsMet = x ∈ V ⟼ d ∈ ℝ * x × x | ∀ y ∈ x y d y = 0 ∧ ∀ z ∈ x ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z