Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-unifsp Unicode version

Definition df-unifsp 25689
Description: Definition of a uniform space. Bourbaki TG II.1 def. 1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. We consider the space is equipped with the topology induced by the uniform structure. (Contributed by FL, 29-May-2014.)
Assertion
Ref Expression
df-unifsp  |-  UnifSp  =  {
f  |  E. y E. x E. t ( ( y  =  (
Base `  f )  /\  x  =  ( Unif `  f )  /\  t  =  ( TopOpen `  f ) )  /\  ( x  C_  ~P (
y  X.  y )  /\  ( y  X.  y )  e.  x  /\  A. v  e.  x  ( A. u  e.  ~P  ( y  X.  y
) ( v  C_  u  ->  u  e.  x
)  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
) )  /\  t  =  ( iota_ s  e. 
Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s ) `  { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) } ) ) ) }
Distinct variable group:    y, f, x, t, v, u, w, s, a, z

Detailed syntax breakdown of Definition df-unifsp
StepHypRef Expression
1 cunifsp 25688 . 2  class  UnifSp
2 vy . . . . . . . . . 10  set  y
32cv 1631 . . . . . . . . 9  class  y
4 vf . . . . . . . . . . 11  set  f
54cv 1631 . . . . . . . . . 10  class  f
6 cbs 13164 . . . . . . . . . 10  class  Base
75, 6cfv 5271 . . . . . . . . 9  class  ( Base `  f )
83, 7wceq 1632 . . . . . . . 8  wff  y  =  ( Base `  f
)
9 vx . . . . . . . . . 10  set  x
109cv 1631 . . . . . . . . 9  class  x
11 cunif 13234 . . . . . . . . . 10  class  Unif
125, 11cfv 5271 . . . . . . . . 9  class  ( Unif `  f )
1310, 12wceq 1632 . . . . . . . 8  wff  x  =  ( Unif `  f
)
14 vt . . . . . . . . . 10  set  t
1514cv 1631 . . . . . . . . 9  class  t
16 ctopn 13342 . . . . . . . . . 10  class  TopOpen
175, 16cfv 5271 . . . . . . . . 9  class  ( TopOpen `  f )
1815, 17wceq 1632 . . . . . . . 8  wff  t  =  ( TopOpen `  f )
198, 13, 18w3a 934 . . . . . . 7  wff  ( y  =  ( Base `  f
)  /\  x  =  ( Unif `  f )  /\  t  =  ( TopOpen
`  f ) )
203, 3cxp 4703 . . . . . . . . . 10  class  ( y  X.  y )
2120cpw 3638 . . . . . . . . 9  class  ~P (
y  X.  y )
2210, 21wss 3165 . . . . . . . 8  wff  x  C_  ~P ( y  X.  y
)
2320, 10wcel 1696 . . . . . . . 8  wff  ( y  X.  y )  e.  x
24 vv . . . . . . . . . . . . . 14  set  v
2524cv 1631 . . . . . . . . . . . . 13  class  v
26 vu . . . . . . . . . . . . . 14  set  u
2726cv 1631 . . . . . . . . . . . . 13  class  u
2825, 27wss 3165 . . . . . . . . . . . 12  wff  v  C_  u
2926, 9wel 1697 . . . . . . . . . . . 12  wff  u  e.  x
3028, 29wi 4 . . . . . . . . . . 11  wff  ( v 
C_  u  ->  u  e.  x )
3130, 26, 21wral 2556 . . . . . . . . . 10  wff  A. u  e.  ~P  ( y  X.  y ) ( v 
C_  u  ->  u  e.  x )
32 vw . . . . . . . . . . . . . 14  set  w
3332cv 1631 . . . . . . . . . . . . 13  class  w
3425, 33cin 3164 . . . . . . . . . . . 12  class  ( v  i^i  w )
3534, 10wcel 1696 . . . . . . . . . . 11  wff  ( v  i^i  w )  e.  x
3635, 32, 10wral 2556 . . . . . . . . . 10  wff  A. w  e.  x  ( v  i^i  w )  e.  x
37 cid 4320 . . . . . . . . . . . . 13  class  _I
3837, 3cres 4707 . . . . . . . . . . . 12  class  (  _I  |`  y )
3938, 25wss 3165 . . . . . . . . . . 11  wff  (  _I  |`  y )  C_  v
4025ccnv 4704 . . . . . . . . . . . 12  class  `' v
4140, 10wcel 1696 . . . . . . . . . . 11  wff  `' v  e.  x
4233, 33ccom 4709 . . . . . . . . . . . . 13  class  ( w  o.  w )
4342, 25wss 3165 . . . . . . . . . . . 12  wff  ( w  o.  w )  C_  v
4443, 32, 10wrex 2557 . . . . . . . . . . 11  wff  E. w  e.  x  ( w  o.  w )  C_  v
4539, 41, 44w3a 934 . . . . . . . . . 10  wff  ( (  _I  |`  y )  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  (
w  o.  w ) 
C_  v )
4631, 36, 45w3a 934 . . . . . . . . 9  wff  ( A. u  e.  ~P  (
y  X.  y ) ( v  C_  u  ->  u  e.  x )  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
)
4746, 24, 10wral 2556 . . . . . . . 8  wff  A. v  e.  x  ( A. u  e.  ~P  (
y  X.  y ) ( v  C_  u  ->  u  e.  x )  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
)
4822, 23, 47w3a 934 . . . . . . 7  wff  ( x 
C_  ~P ( y  X.  y )  /\  (
y  X.  y )  e.  x  /\  A. v  e.  x  ( A. u  e.  ~P  ( y  X.  y
) ( v  C_  u  ->  u  e.  x
)  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
) )
49 vs . . . . . . . . . . . . 13  set  s
5049cv 1631 . . . . . . . . . . . 12  class  s
5150cuni 3843 . . . . . . . . . . 11  class  U. s
5251, 3wceq 1632 . . . . . . . . . 10  wff  U. s  =  y
53 va . . . . . . . . . . . . . . 15  set  a
5453cv 1631 . . . . . . . . . . . . . 14  class  a
5554csn 3653 . . . . . . . . . . . . 13  class  { a }
56 cnei 16850 . . . . . . . . . . . . . 14  class  nei
5750, 56cfv 5271 . . . . . . . . . . . . 13  class  ( nei `  s )
5855, 57cfv 5271 . . . . . . . . . . . 12  class  ( ( nei `  s ) `
 { a } )
59 vz . . . . . . . . . . . . . . . 16  set  z
6059cv 1631 . . . . . . . . . . . . . . 15  class  z
6127, 55cima 4708 . . . . . . . . . . . . . . 15  class  ( u
" { a } )
6260, 61wceq 1632 . . . . . . . . . . . . . 14  wff  z  =  ( u " {
a } )
6362, 26, 10wrex 2557 . . . . . . . . . . . . 13  wff  E. u  e.  x  z  =  ( u " {
a } )
6463, 59cab 2282 . . . . . . . . . . . 12  class  { z  |  E. u  e.  x  z  =  ( u " { a } ) }
6558, 64wceq 1632 . . . . . . . . . . 11  wff  ( ( nei `  s ) `
 { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) }
6665, 53, 3wral 2556 . . . . . . . . . 10  wff  A. a  e.  y  ( ( nei `  s ) `  { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) }
6752, 66wa 358 . . . . . . . . 9  wff  ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s
) `  { a } )  =  {
z  |  E. u  e.  x  z  =  ( u " {
a } ) } )
68 ctop 16647 . . . . . . . . 9  class  Top
6967, 49, 68crio 6313 . . . . . . . 8  class  ( iota_ s  e.  Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s
) `  { a } )  =  {
z  |  E. u  e.  x  z  =  ( u " {
a } ) } ) )
7015, 69wceq 1632 . . . . . . 7  wff  t  =  ( iota_ s  e.  Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s ) `  {
a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) } ) )
7119, 48, 70w3a 934 . . . . . 6  wff  ( ( y  =  ( Base `  f )  /\  x  =  ( Unif `  f
)  /\  t  =  ( TopOpen `  f )
)  /\  ( x  C_ 
~P ( y  X.  y )  /\  (
y  X.  y )  e.  x  /\  A. v  e.  x  ( A. u  e.  ~P  ( y  X.  y
) ( v  C_  u  ->  u  e.  x
)  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
) )  /\  t  =  ( iota_ s  e. 
Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s ) `  { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) } ) ) )
7271, 14wex 1531 . . . . 5  wff  E. t
( ( y  =  ( Base `  f
)  /\  x  =  ( Unif `  f )  /\  t  =  ( TopOpen
`  f ) )  /\  ( x  C_  ~P ( y  X.  y
)  /\  ( y  X.  y )  e.  x  /\  A. v  e.  x  ( A. u  e.  ~P  ( y  X.  y
) ( v  C_  u  ->  u  e.  x
)  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
) )  /\  t  =  ( iota_ s  e. 
Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s ) `  { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) } ) ) )
7372, 9wex 1531 . . . 4  wff  E. x E. t ( ( y  =  ( Base `  f
)  /\  x  =  ( Unif `  f )  /\  t  =  ( TopOpen
`  f ) )  /\  ( x  C_  ~P ( y  X.  y
)  /\  ( y  X.  y )  e.  x  /\  A. v  e.  x  ( A. u  e.  ~P  ( y  X.  y
) ( v  C_  u  ->  u  e.  x
)  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
) )  /\  t  =  ( iota_ s  e. 
Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s ) `  { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) } ) ) )
7473, 2wex 1531 . . 3  wff  E. y E. x E. t ( ( y  =  (
Base `  f )  /\  x  =  ( Unif `  f )  /\  t  =  ( TopOpen `  f ) )  /\  ( x  C_  ~P (
y  X.  y )  /\  ( y  X.  y )  e.  x  /\  A. v  e.  x  ( A. u  e.  ~P  ( y  X.  y
) ( v  C_  u  ->  u  e.  x
)  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
) )  /\  t  =  ( iota_ s  e. 
Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s ) `  { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) } ) ) )
7574, 4cab 2282 . 2  class  { f  |  E. y E. x E. t ( ( y  =  (
Base `  f )  /\  x  =  ( Unif `  f )  /\  t  =  ( TopOpen `  f ) )  /\  ( x  C_  ~P (
y  X.  y )  /\  ( y  X.  y )  e.  x  /\  A. v  e.  x  ( A. u  e.  ~P  ( y  X.  y
) ( v  C_  u  ->  u  e.  x
)  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
) )  /\  t  =  ( iota_ s  e. 
Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s ) `  { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) } ) ) ) }
761, 75wceq 1632 1  wff  UnifSp  =  {
f  |  E. y E. x E. t ( ( y  =  (
Base `  f )  /\  x  =  ( Unif `  f )  /\  t  =  ( TopOpen `  f ) )  /\  ( x  C_  ~P (
y  X.  y )  /\  ( y  X.  y )  e.  x  /\  A. v  e.  x  ( A. u  e.  ~P  ( y  X.  y
) ( v  C_  u  ->  u  e.  x
)  /\  A. w  e.  x  ( v  i^i  w )  e.  x  /\  ( (  _I  |`  y
)  C_  v  /\  `' v  e.  x  /\  E. w  e.  x  ( w  o.  w
)  C_  v )
) )  /\  t  =  ( iota_ s  e. 
Top ( U. s  =  y  /\  A. a  e.  y  ( ( nei `  s ) `  { a } )  =  { z  |  E. u  e.  x  z  =  ( u " { a } ) } ) ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator