Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-utop Unicode version

Definition df-utop 18214
 Description: Definition of a topology induced by a uniform structure. Definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
Assertion
Ref Expression
df-utop unifTop UnifOn
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-utop
StepHypRef Expression
1 cutop 18213 . 2 unifTop
2 vu . . 3
3 cust 18182 . . . . 5 UnifOn
43crn 4838 . . . 4 UnifOn
54cuni 3975 . . 3 UnifOn
6 vv . . . . . . . . 9
76cv 1648 . . . . . . . 8
8 vx . . . . . . . . . 10
98cv 1648 . . . . . . . . 9
109csn 3774 . . . . . . . 8
117, 10cima 4840 . . . . . . 7
12 va . . . . . . . 8
1312cv 1648 . . . . . . 7
1411, 13wss 3280 . . . . . 6
152cv 1648 . . . . . 6
1614, 6, 15wrex 2667 . . . . 5
1716, 8, 13wral 2666 . . . 4
1815cuni 3975 . . . . . 6
1918cdm 4837 . . . . 5
2019cpw 3759 . . . 4
2117, 12, 20crab 2670 . . 3
222, 5, 21cmpt 4226 . 2 UnifOn
231, 22wceq 1649 1 unifTop UnifOn
 Colors of variables: wff set class This definition is referenced by:  utopval  18215
 Copyright terms: Public domain W3C validator