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

Metamath Proof Explorer

Definition df-cfil

Description: Define the set of Cauchy filters on a given extended metric space. A Cauchy filter is a filter on the set such that for every 0 < x there is an element of the filter whose metric diameter is less than x . (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion df-cfil 
|- CauFil = ( d e. U. ran *Met |-> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccfil 
 |-  CauFil
1 vd 
 |-  d
2 cxmet 
 |-  *Met
3 2 crn 
 |-  ran *Met
4 3 cuni 
 |-  U. ran *Met
5 vf 
 |-  f
6 cfil 
 |-  Fil
7 1 cv 
 |-  d
8 7 cdm 
 |-  dom d
9 8 cdm 
 |-  dom dom d
10 9 6 cfv 
 |-  ( Fil ` dom dom d )
11 vx 
 |-  x
12 crp 
 |-  RR+
13 vy 
 |-  y
14 5 cv 
 |-  f
15 13 cv 
 |-  y
16 15 15 cxp 
 |-  ( y X. y )
17 7 16 cima 
 |-  ( d " ( y X. y ) )
18 cc0 
 |-  0
19 cico 
 |-  [,)
20 11 cv 
 |-  x
21 18 20 19 co 
 |-  ( 0 [,) x )
22 17 21 wss 
 |-  ( d " ( y X. y ) ) C_ ( 0 [,) x )
23 22 13 14 wrex 
 |-  E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
24 23 11 12 wral 
 |-  A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x )
25 24 5 10 crab 
 |-  { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) }
26 1 4 25 cmpt 
 |-  ( d e. U. ran *Met |-> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } )
27 0 26 wceq 
 |-  CauFil = ( d e. U. ran *Met |-> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } )