Metamath Proof Explorer

Theorem cfilfval

Description: The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion cfilfval 
|- ( D e. ( *Met ` X ) -> ( CauFil ` D ) = { f e. ( Fil ` X ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } )

Proof

Step Hyp Ref Expression
1 fvssunirn 
 |-  ( *Met ` X ) C_ U. ran *Met
2 1 sseli 
 |-  ( D e. ( *Met ` X ) -> D e. U. ran *Met )
3 dmeq 
 |-  ( d = D -> dom d = dom D )
4 3 dmeqd 
 |-  ( d = D -> dom dom d = dom dom D )
5 4 fveq2d 
 |-  ( d = D -> ( Fil ` dom dom d ) = ( Fil ` dom dom D ) )
6 imaeq1 
 |-  ( d = D -> ( d " ( y X. y ) ) = ( D " ( y X. y ) ) )
7 6 sseq1d 
 |-  ( d = D -> ( ( d " ( y X. y ) ) C_ ( 0 [,) x ) <-> ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
8 7 rexbidv 
 |-  ( d = D -> ( E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) <-> E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
9 8 ralbidv 
 |-  ( d = D -> ( A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) <-> A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
10 5 9 rabeqbidv 
 |-  ( d = D -> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } = { f e. ( Fil ` dom dom D ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } )
11 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 ) } )
12 fvex 
 |-  ( Fil ` dom dom D ) e. _V
13 12 rabex 
 |-  { f e. ( Fil ` dom dom D ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } e. _V
14 10 11 13 fvmpt 
 |-  ( D e. U. ran *Met -> ( CauFil ` D ) = { f e. ( Fil ` dom dom D ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } )
15 2 14 syl 
 |-  ( D e. ( *Met ` X ) -> ( CauFil ` D ) = { f e. ( Fil ` dom dom D ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } )
16 xmetdmdm 
 |-  ( D e. ( *Met ` X ) -> X = dom dom D )
17 16 fveq2d 
 |-  ( D e. ( *Met ` X ) -> ( Fil ` X ) = ( Fil ` dom dom D ) )
18 17 rabeqdv 
 |-  ( D e. ( *Met ` X ) -> { f e. ( Fil ` X ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } = { f e. ( Fil ` dom dom D ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } )
19 15 18 eqtr4d 
 |-  ( D e. ( *Met ` X ) -> ( CauFil ` D ) = { f e. ( Fil ` X ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } )