Detailed syntax breakdown of Definition df-metu
Step | Hyp | Ref
| Expression |
1 | | cmetu 20210 |
. 2
class
metUnif |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cpsmet 20203 |
. . . . 5
class
PsMet |
4 | 3 | crn 5526 |
. . . 4
class ran
PsMet |
5 | 4 | cuni 4796 |
. . 3
class ∪ ran PsMet |
6 | 2 | cv 1541 |
. . . . . . 7
class 𝑑 |
7 | 6 | cdm 5525 |
. . . . . 6
class dom 𝑑 |
8 | 7 | cdm 5525 |
. . . . 5
class dom dom
𝑑 |
9 | 8, 8 | cxp 5523 |
. . . 4
class (dom dom
𝑑 × dom dom 𝑑) |
10 | | va |
. . . . . 6
setvar 𝑎 |
11 | | crp 12474 |
. . . . . 6
class
ℝ+ |
12 | 6 | ccnv 5524 |
. . . . . . 7
class ◡𝑑 |
13 | | cc0 10617 |
. . . . . . . 8
class
0 |
14 | 10 | cv 1541 |
. . . . . . . 8
class 𝑎 |
15 | | cico 12825 |
. . . . . . . 8
class
[,) |
16 | 13, 14, 15 | co 7172 |
. . . . . . 7
class
(0[,)𝑎) |
17 | 12, 16 | cima 5528 |
. . . . . 6
class (◡𝑑 “ (0[,)𝑎)) |
18 | 10, 11, 17 | cmpt 5110 |
. . . . 5
class (𝑎 ∈ ℝ+
↦ (◡𝑑 “ (0[,)𝑎))) |
19 | 18 | crn 5526 |
. . . 4
class ran
(𝑎 ∈
ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) |
20 | | cfg 20208 |
. . . 4
class
filGen |
21 | 9, 19, 20 | co 7172 |
. . 3
class ((dom dom
𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))) |
22 | 2, 5, 21 | cmpt 5110 |
. 2
class (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |
23 | 1, 22 | wceq 1542 |
1
wff metUnif =
(𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |