Step | Hyp | Ref
| Expression |
1 | | cmetu 21226 |
. 2
class
metUnif |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cpsmet 21219 |
. . . . 5
class
PsMet |
4 | 3 | crn 5670 |
. . . 4
class ran
PsMet |
5 | 4 | cuni 4902 |
. . 3
class ∪ ran PsMet |
6 | 2 | cv 1532 |
. . . . . . 7
class 𝑑 |
7 | 6 | cdm 5669 |
. . . . . 6
class dom 𝑑 |
8 | 7 | cdm 5669 |
. . . . 5
class dom dom
𝑑 |
9 | 8, 8 | cxp 5667 |
. . . 4
class (dom dom
𝑑 × dom dom 𝑑) |
10 | | va |
. . . . . 6
setvar 𝑎 |
11 | | crp 12977 |
. . . . . 6
class
ℝ+ |
12 | 6 | ccnv 5668 |
. . . . . . 7
class ◡𝑑 |
13 | | cc0 11109 |
. . . . . . . 8
class
0 |
14 | 10 | cv 1532 |
. . . . . . . 8
class 𝑎 |
15 | | cico 13329 |
. . . . . . . 8
class
[,) |
16 | 13, 14, 15 | co 7404 |
. . . . . . 7
class
(0[,)𝑎) |
17 | 12, 16 | cima 5672 |
. . . . . 6
class (◡𝑑 “ (0[,)𝑎)) |
18 | 10, 11, 17 | cmpt 5224 |
. . . . 5
class (𝑎 ∈ ℝ+
↦ (◡𝑑 “ (0[,)𝑎))) |
19 | 18 | crn 5670 |
. . . 4
class ran
(𝑎 ∈
ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) |
20 | | cfg 21224 |
. . . 4
class
filGen |
21 | 9, 19, 20 | co 7404 |
. . 3
class ((dom dom
𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))) |
22 | 2, 5, 21 | cmpt 5224 |
. 2
class (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |
23 | 1, 22 | wceq 1533 |
1
wff metUnif =
(𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |