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

Definition df-ust 19773
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 definition 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 19772 . 2  class UnifOn
2 vx . . 3  setvar  x
3 cvv 2970 . . 3  class  _V
4 vu . . . . . . 7  setvar  u
54cv 1368 . . . . . 6  class  u
62cv 1368 . . . . . . . 8  class  x
76, 6cxp 4836 . . . . . . 7  class  ( x  X.  x )
87cpw 3858 . . . . . 6  class  ~P (
x  X.  x )
95, 8wss 3326 . . . . 5  wff  u  C_  ~P ( x  X.  x
)
107, 5wcel 1756 . . . . 5  wff  ( x  X.  x )  e.  u
11 vv . . . . . . . . . . 11  setvar  v
1211cv 1368 . . . . . . . . . 10  class  v
13 vw . . . . . . . . . . 11  setvar  w
1413cv 1368 . . . . . . . . . 10  class  w
1512, 14wss 3326 . . . . . . . . 9  wff  v  C_  w
1613, 4wel 1757 . . . . . . . . 9  wff  w  e.  u
1715, 16wi 4 . . . . . . . 8  wff  ( v 
C_  w  ->  w  e.  u )
1817, 13, 8wral 2713 . . . . . . 7  wff  A. w  e.  ~P  ( x  X.  x ) ( v 
C_  w  ->  w  e.  u )
1912, 14cin 3325 . . . . . . . . 9  class  ( v  i^i  w )
2019, 5wcel 1756 . . . . . . . 8  wff  ( v  i^i  w )  e.  u
2120, 13, 5wral 2713 . . . . . . 7  wff  A. w  e.  u  ( v  i^i  w )  e.  u
22 cid 4629 . . . . . . . . . 10  class  _I
2322, 6cres 4840 . . . . . . . . 9  class  (  _I  |`  x )
2423, 12wss 3326 . . . . . . . 8  wff  (  _I  |`  x )  C_  v
2512ccnv 4837 . . . . . . . . 9  class  `' v
2625, 5wcel 1756 . . . . . . . 8  wff  `' v  e.  u
2714, 14ccom 4842 . . . . . . . . . 10  class  ( w  o.  w )
2827, 12wss 3326 . . . . . . . . 9  wff  ( w  o.  w )  C_  v
2928, 13, 5wrex 2714 . . . . . . . 8  wff  E. w  e.  u  ( w  o.  w )  C_  v
3024, 26, 29w3a 965 . . . . . . 7  wff  ( (  _I  |`  x )  C_  v  /\  `' v  e.  u  /\  E. w  e.  u  (
w  o.  w ) 
C_  v )
3118, 21, 30w3a 965 . . . . . 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 2713 . . . . 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 965 . . . 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 2427 . . 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 4348 . 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 1369 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 setvar class
This definition is referenced by:  ustfn  19774  ustval  19775  ustn0  19793
  Copyright terms: Public domain W3C validator