Metamath Proof Explorer

Definition df-xmet

Description: Define the set of all extended metrics on a given base set. The definition is similar to df-met , but we also allow the metric to take on the value +oo . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion df-xmet ⊢ ∞Met = x ∈ V ⟼ d ∈ ℝ * x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxmet class ∞Met
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 vz setvar z
11 9 cv setvar y
12 3 cv setvar d
13 10 cv setvar z
14 11 13 12 co class y d z
15 cc0 class 0
16 14 15 wceq wff y d z = 0
17 11 13 wceq wff y = z
18 16 17 wb wff y d z = 0 ↔ y = z
19 vw setvar w
20 cle class ≤
21 19 cv setvar w
22 21 11 12 co class w d y
23 cxad class + 𝑒
24 21 13 12 co class w d z
25 22 24 23 co class w d y + 𝑒 w d z
26 14 25 20 wbr wff y d z ≤ w d y + 𝑒 w d z
27 26 19 6 wral wff ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
28 18 27 wa wff y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
29 28 10 6 wral wff ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
30 29 9 6 wral wff ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
31 30 3 8 crab class d ∈ ℝ * x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
32 1 2 31 cmpt class x ∈ V ⟼ d ∈ ℝ * x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
33 0 32 wceq wff ∞Met = x ∈ V ⟼ d ∈ ℝ * x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z