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

Definition df-ust 18183
 Description: Definition of a uniform structure. Definition 1 of [BourbakiTop1] p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This defintion is analogous to TopOn. Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014.) (Revised by Thierry Arnoux, 15-Nov-2017.)
Assertion
Ref Expression
df-ust UnifOn
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-ust
StepHypRef Expression
1 cust 18182 . 2 UnifOn
2 vx . . 3
3 cvv 2916 . . 3
4 vu . . . . . . 7
54cv 1648 . . . . . 6
62cv 1648 . . . . . . . 8
76, 6cxp 4835 . . . . . . 7
87cpw 3759 . . . . . 6
95, 8wss 3280 . . . . 5
107, 5wcel 1721 . . . . 5
11 vv . . . . . . . . . . 11
1211cv 1648 . . . . . . . . . 10
13 vw . . . . . . . . . . 11
1413cv 1648 . . . . . . . . . 10
1512, 14wss 3280 . . . . . . . . 9
1613, 4wel 1722 . . . . . . . . 9
1715, 16wi 4 . . . . . . . 8
1817, 13, 8wral 2666 . . . . . . 7
1912, 14cin 3279 . . . . . . . . 9
2019, 5wcel 1721 . . . . . . . 8
2120, 13, 5wral 2666 . . . . . . 7
22 cid 4453 . . . . . . . . . 10
2322, 6cres 4839 . . . . . . . . 9
2423, 12wss 3280 . . . . . . . 8
2512ccnv 4836 . . . . . . . . 9
2625, 5wcel 1721 . . . . . . . 8
2714, 14ccom 4841 . . . . . . . . . 10
2827, 12wss 3280 . . . . . . . . 9
2928, 13, 5wrex 2667 . . . . . . . 8
3024, 26, 29w3a 936 . . . . . . 7
3118, 21, 30w3a 936 . . . . . 6
3231, 11, 5wral 2666 . . . . 5
339, 10, 32w3a 936 . . . 4
3433, 4cab 2390 . . 3
352, 3, 34cmpt 4226 . 2
361, 35wceq 1649 1 UnifOn
 Colors of variables: wff set class This definition is referenced by:  ustfn  18184  ustval  18185  ustn0  18203
 Copyright terms: Public domain W3C validator