Step | Hyp | Ref
| Expression |
1 | | cmetu 13416 |
. 2
class
metUnif |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cpsmet 13409 |
. . . . 5
class
PsMet |
4 | 3 | crn 4627 |
. . . 4
class ran
PsMet |
5 | 4 | cuni 3809 |
. . 3
class ∪ ran PsMet |
6 | 2 | cv 1352 |
. . . . . . 7
class 𝑑 |
7 | 6 | cdm 4626 |
. . . . . 6
class dom 𝑑 |
8 | 7 | cdm 4626 |
. . . . 5
class dom dom
𝑑 |
9 | 8, 8 | cxp 4624 |
. . . 4
class (dom dom
𝑑 × dom dom 𝑑) |
10 | | va |
. . . . . 6
setvar 𝑎 |
11 | | crp 9652 |
. . . . . 6
class
ℝ+ |
12 | 6 | ccnv 4625 |
. . . . . . 7
class ◡𝑑 |
13 | | cc0 7810 |
. . . . . . . 8
class
0 |
14 | 10 | cv 1352 |
. . . . . . . 8
class 𝑎 |
15 | | cico 9889 |
. . . . . . . 8
class
[,) |
16 | 13, 14, 15 | co 5874 |
. . . . . . 7
class
(0[,)𝑎) |
17 | 12, 16 | cima 4629 |
. . . . . 6
class (◡𝑑 “ (0[,)𝑎)) |
18 | 10, 11, 17 | cmpt 4064 |
. . . . 5
class (𝑎 ∈ ℝ+
↦ (◡𝑑 “ (0[,)𝑎))) |
19 | 18 | crn 4627 |
. . . 4
class ran
(𝑎 ∈
ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) |
20 | | cfg 13414 |
. . . 4
class
filGen |
21 | 9, 19, 20 | co 5874 |
. . 3
class ((dom dom
𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))) |
22 | 2, 5, 21 | cmpt 4064 |
. 2
class (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |
23 | 1, 22 | wceq 1353 |
1
wff metUnif =
(𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |