MPE Home 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  =  ( x  e.  _V  |->  { u  |  ( u 
C_  ~P ( x  X.  x )  /\  (
x  X.  x )  e.  u  /\  A. v  e.  u  ( A. w  e.  ~P  ( x  X.  x
) ( v  C_  w  ->  w  e.  u
)  /\  A. w  e.  u  ( v  i^i  w )  e.  u  /\  ( (  _I  |`  x
)  C_  v  /\  `' v  e.  u  /\  E. w  e.  u  ( w  o.  w
)  C_  v )
) ) } )
Distinct variable group:    x, u, v, w

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