Description: Definition of a topology induced by a uniform structure. Definition 3 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | df-utop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cutop | |
|
1 | vu | |
|
2 | cust | |
|
3 | 2 | crn | |
4 | 3 | cuni | |
5 | va | |
|
6 | 1 | cv | |
7 | 6 | cuni | |
8 | 7 | cdm | |
9 | 8 | cpw | |
10 | vx | |
|
11 | 5 | cv | |
12 | vv | |
|
13 | 12 | cv | |
14 | 10 | cv | |
15 | 14 | csn | |
16 | 13 15 | cima | |
17 | 16 11 | wss | |
18 | 17 12 6 | wrex | |
19 | 18 10 11 | wral | |
20 | 19 5 9 | crab | |
21 | 1 4 20 | cmpt | |
22 | 0 21 | wceq | |