This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cfilu

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)

Ref Expression
Assertion 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 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccfilu 
 |-  CauFilU
1 vu 
 |-  u
2 cust 
 |-  UnifOn
3 2 crn 
 |-  ran UnifOn
4 3 cuni 
 |-  U. ran UnifOn
5 vf 
 |-  f
6 cfbas 
 |-  fBas
7 1 cv 
 |-  u
8 7 cuni 
 |-  U. u
9 8 cdm 
 |-  dom U. u
10 9 6 cfv 
 |-  ( fBas ` dom U. u )
11 vv 
 |-  v
12 va 
 |-  a
13 5 cv 
 |-  f
14 12 cv 
 |-  a
15 14 14 cxp 
 |-  ( a X. a )
16 11 cv 
 |-  v
17 15 16 wss 
 |-  ( a X. a ) C_ v
18 17 12 13 wrex 
 |-  E. a e. f ( a X. a ) C_ v
19 18 11 7 wral 
 |-  A. v e. u E. a e. f ( a X. a ) C_ v
20 19 5 10 crab 
 |-  { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v }
21 1 4 20 cmpt 
 |-  ( u e. U. ran UnifOn |-> { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v } )
22 0 21 wceq 
 |-  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 } )