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

Definition df-cfilu 20660
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 20659 . 2  class CauFilu
2 vu . . 3  setvar  u
3 cust 20572 . . . . 5  class UnifOn
43crn 4987 . . . 4  class  ran UnifOn
54cuni 4231 . . 3  class  U. ran UnifOn
6 va . . . . . . . . 9  setvar  a
76cv 1380 . . . . . . . 8  class  a
87, 7cxp 4984 . . . . . . 7  class  ( a  X.  a )
9 vv . . . . . . . 8  setvar  v
109cv 1380 . . . . . . 7  class  v
118, 10wss 3459 . . . . . 6  wff  ( a  X.  a )  C_  v
12 vf . . . . . . 7  setvar  f
1312cv 1380 . . . . . 6  class  f
1411, 6, 13wrex 2792 . . . . 5  wff  E. a  e.  f  ( a  X.  a )  C_  v
152cv 1380 . . . . 5  class  u
1614, 9, 15wral 2791 . . . 4  wff  A. v  e.  u  E. a  e.  f  ( a  X.  a )  C_  v
1715cuni 4231 . . . . . 6  class  U. u
1817cdm 4986 . . . . 5  class  dom  U. u
19 cfbas 18277 . . . . 5  class  fBas
2018, 19cfv 5575 . . . 4  class  ( fBas `  dom  U. u )
2116, 12, 20crab 2795 . . 3  class  { f  e.  ( fBas `  dom  U. u )  |  A. v  e.  u  E. a  e.  f  (
a  X.  a ) 
C_  v }
222, 5, 21cmpt 4492 . 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 1381 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  20661
  Copyright terms: Public domain W3C validator