Metamath Proof Explorer

Theorem cfili

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

Ref Expression
Assertion cfili 
|- ( ( F e. ( CauFil ` D ) /\ R e. RR+ ) -> E. x e. F A. y e. x A. z e. x ( y D z ) < R )

Proof

Step Hyp Ref Expression
1 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 ) } )
2 1 mptrcl 
 |-  ( F e. ( CauFil ` D ) -> D e. U. ran *Met )
3 xmetunirn 
 |-  ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
4 2 3 sylib 
 |-  ( F e. ( CauFil ` D ) -> D e. ( *Met ` dom dom D ) )
5 iscfil2 
 |-  ( D e. ( *Met ` dom dom D ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` dom dom D ) /\ A. r e. RR+ E. x e. F A. y e. x A. z e. x ( y D z ) < r ) ) )
6 4 5 syl 
 |-  ( F e. ( CauFil ` D ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` dom dom D ) /\ A. r e. RR+ E. x e. F A. y e. x A. z e. x ( y D z ) < r ) ) )
7 6 ibi 
 |-  ( F e. ( CauFil ` D ) -> ( F e. ( Fil ` dom dom D ) /\ A. r e. RR+ E. x e. F A. y e. x A. z e. x ( y D z ) < r ) )
8 7 simprd 
 |-  ( F e. ( CauFil ` D ) -> A. r e. RR+ E. x e. F A. y e. x A. z e. x ( y D z ) < r )
9 breq2 
 |-  ( r = R -> ( ( y D z ) < r <-> ( y D z ) < R ) )
10 9 2ralbidv 
 |-  ( r = R -> ( A. y e. x A. z e. x ( y D z ) < r <-> A. y e. x A. z e. x ( y D z ) < R ) )
11 10 rexbidv 
 |-  ( r = R -> ( E. x e. F A. y e. x A. z e. x ( y D z ) < r <-> E. x e. F A. y e. x A. z e. x ( y D z ) < R ) )
12 11 rspccva 
 |-  ( ( A. r e. RR+ E. x e. F A. y e. x A. z e. x ( y D z ) < r /\ R e. RR+ ) -> E. x e. F A. y e. x A. z e. x ( y D z ) < R )
13 8 12 sylan 
 |-  ( ( F e. ( CauFil ` D ) /\ R e. RR+ ) -> E. x e. F A. y e. x A. z e. x ( y D z ) < R )