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

Metamath Proof Explorer

Theorem iscfil

Description: The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion iscfil 
|- ( D e. ( *Met ` X ) -> ( F e. ( 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 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 ) } )
2 1 eleq2d 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> F e. { f e. ( Fil ` X ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } ) )
3 rexeq 
 |-  ( f = F -> ( E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> E. y e. F ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
4 3 ralbidv 
 |-  ( f = F -> ( 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 ) ) )
5 4 elrab 
 |-  ( F e. { f e. ( Fil ` X ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
6 2 5 bitrdi 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )