Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-metu | Unicode version |
Description: Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
Ref | Expression |
---|---|
df-metu | metUnif PsMet |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmetu 12155 | . 2 metUnif | |
2 | vd | . . 3 | |
3 | cpsmet 12148 | . . . . 5 PsMet | |
4 | 3 | crn 4540 | . . . 4 PsMet |
5 | 4 | cuni 3736 | . . 3 PsMet |
6 | 2 | cv 1330 | . . . . . . 7 |
7 | 6 | cdm 4539 | . . . . . 6 |
8 | 7 | cdm 4539 | . . . . 5 |
9 | 8, 8 | cxp 4537 | . . . 4 |
10 | va | . . . . . 6 | |
11 | crp 9441 | . . . . . 6 | |
12 | 6 | ccnv 4538 | . . . . . . 7 |
13 | cc0 7620 | . . . . . . . 8 | |
14 | 10 | cv 1330 | . . . . . . . 8 |
15 | cico 9673 | . . . . . . . 8 | |
16 | 13, 14, 15 | co 5774 | . . . . . . 7 |
17 | 12, 16 | cima 4542 | . . . . . 6 |
18 | 10, 11, 17 | cmpt 3989 | . . . . 5 |
19 | 18 | crn 4540 | . . . 4 |
20 | cfg 12153 | . . . 4 | |
21 | 9, 19, 20 | co 5774 | . . 3 |
22 | 2, 5, 21 | cmpt 3989 | . 2 PsMet |
23 | 1, 22 | wceq 1331 | 1 metUnif PsMet |
Colors of variables: wff set class |
This definition is referenced by: (None) |
Copyright terms: Public domain | W3C validator |