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

Definition df-cfilu 19877
Description: Define the set of Cauchy filter bases on a uniform space. A Cauchy filter base is a filter base on the set such that for every entourage  v, there is an element  a of the filter "small enough in  v " i.e. such that every pair  { x ,  y } of points in  a is related by  v". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.)
Assertion
Ref Expression
df-cfilu  |- CauFilu  =  ( u  e.  U. ran UnifOn  |->  { f  e.  ( fBas `  dom  U. u )  |  A. v  e.  u  E. a  e.  f  (
a  X.  a ) 
C_  v } )
Distinct variable group:    u, f, v, a

Detailed syntax breakdown of Definition df-cfilu
StepHypRef Expression
1 ccfilu 19876 . 2  class CauFilu
2 vu . . 3  setvar  u
3 cust 19789 . . . . 5  class UnifOn
43crn 4856 . . . 4  class  ran UnifOn
54cuni 4106 . . 3  class  U. ran UnifOn
6 va . . . . . . . . 9  setvar  a
76cv 1368 . . . . . . . 8  class  a
87, 7cxp 4853 . . . . . . 7  class  ( a  X.  a )
9 vv . . . . . . . 8  setvar  v
109cv 1368 . . . . . . 7  class  v
118, 10wss 3343 . . . . . 6  wff  ( a  X.  a )  C_  v
12 vf . . . . . . 7  setvar  f
1312cv 1368 . . . . . 6  class  f
1411, 6, 13wrex 2731 . . . . 5  wff  E. a  e.  f  ( a  X.  a )  C_  v
152cv 1368 . . . . 5  class  u
1614, 9, 15wral 2730 . . . 4  wff  A. v  e.  u  E. a  e.  f  ( a  X.  a )  C_  v
1715cuni 4106 . . . . . 6  class  U. u
1817cdm 4855 . . . . 5  class  dom  U. u
19 cfbas 17819 . . . . 5  class  fBas
2018, 19cfv 5433 . . . 4  class  ( fBas `  dom  U. u )
2116, 12, 20crab 2734 . . 3  class  { f  e.  ( fBas `  dom  U. u )  |  A. v  e.  u  E. a  e.  f  (
a  X.  a ) 
C_  v }
222, 5, 21cmpt 4365 . 2  class  ( u  e.  U. ran UnifOn  |->  { f  e.  ( fBas `  dom  U. u )  |  A. v  e.  u  E. a  e.  f  (
a  X.  a ) 
C_  v } )
231, 22wceq 1369 1  wff CauFilu  =  ( u  e.  U. ran UnifOn  |->  { f  e.  ( fBas `  dom  U. u )  |  A. v  e.  u  E. a  e.  f  (
a  X.  a ) 
C_  v } )
Colors of variables: wff setvar class
This definition is referenced by:  iscfilu  19878
  Copyright terms: Public domain W3C validator