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∈xydz=0↔y=z∧∀w∈xydz≤wdy+𝑒wdz

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxmet class∞Met
1 vx setvarx
2 cvv classV
3 vd setvard
4 cxr classℝ*
5 cmap class↑𝑚
6 1 cv setvarx
7 6 6 cxp classx×x
8 4 7 5 co classℝ*x×x
9 vy setvary
10 vz setvarz
11 9 cv setvary
12 3 cv setvard
13 10 cv setvarz
14 11 13 12 co classydz
15 cc0 class0
16 14 15 wceq wffydz=0
17 11 13 wceq wffy=z
18 16 17 wb wffydz=0↔y=z
19 vw setvarw
20 cle class≤
21 19 cv setvarw
22 21 11 12 co classwdy
23 cxad class+𝑒
24 21 13 12 co classwdz
25 22 24 23 co classwdy+𝑒wdz
26 14 25 20 wbr wffydz≤wdy+𝑒wdz
27 26 19 6 wral wff∀w∈xydz≤wdy+𝑒wdz
28 18 27 wa wffydz=0↔y=z∧∀w∈xydz≤wdy+𝑒wdz
29 28 10 6 wral wff∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+𝑒wdz
30 29 9 6 wral wff∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+𝑒wdz
31 30 3 8 crab classd∈ℝ*x×x|∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+𝑒wdz
32 1 2 31 cmpt classx∈V⟼d∈ℝ*x×x|∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+𝑒wdz
33 0 32 wceq wff∞Met=x∈V⟼d∈ℝ*x×x|∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+𝑒wdz