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

Definition df-utop 20900
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  =  ( u  e.  U. ran UnifOn  |->  { a  e.  ~P dom  U. u  |  A. x  e.  a  E. v  e.  u  ( v " { x } ) 
C_  a } )
Distinct variable group:    u, a, v, x

Detailed syntax breakdown of Definition df-utop
StepHypRef Expression
1 cutop 20899 . 2  class unifTop
2 vu . . 3  setvar  u
3 cust 20868 . . . . 5  class UnifOn
43crn 4989 . . . 4  class  ran UnifOn
54cuni 4235 . . 3  class  U. ran UnifOn
6 vv . . . . . . . . 9  setvar  v
76cv 1397 . . . . . . . 8  class  v
8 vx . . . . . . . . . 10  setvar  x
98cv 1397 . . . . . . . . 9  class  x
109csn 4016 . . . . . . . 8  class  { x }
117, 10cima 4991 . . . . . . 7  class  ( v
" { x }
)
12 va . . . . . . . 8  setvar  a
1312cv 1397 . . . . . . 7  class  a
1411, 13wss 3461 . . . . . 6  wff  ( v
" { x }
)  C_  a
152cv 1397 . . . . . 6  class  u
1614, 6, 15wrex 2805 . . . . 5  wff  E. v  e.  u  ( v " { x } ) 
C_  a
1716, 8, 13wral 2804 . . . 4  wff  A. x  e.  a  E. v  e.  u  ( v " { x } ) 
C_  a
1815cuni 4235 . . . . . 6  class  U. u
1918cdm 4988 . . . . 5  class  dom  U. u
2019cpw 3999 . . . 4  class  ~P dom  U. u
2117, 12, 20crab 2808 . . 3  class  { a  e.  ~P dom  U. u  |  A. x  e.  a  E. v  e.  u  ( v " { x } ) 
C_  a }
222, 5, 21cmpt 4497 . 2  class  ( u  e.  U. ran UnifOn  |->  { a  e.  ~P dom  U. u  |  A. x  e.  a  E. v  e.  u  ( v " { x } ) 
C_  a } )
231, 22wceq 1398 1  wff unifTop  =  ( u  e.  U. ran UnifOn  |->  { a  e.  ~P dom  U. u  |  A. x  e.  a  E. v  e.  u  ( v " { x } ) 
C_  a } )
Colors of variables: wff setvar class
This definition is referenced by:  utopval  20901
  Copyright terms: Public domain W3C validator