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 ∞Met X F CauFil D F Fil X x + y F D y × y 0 x

Proof

Step Hyp Ref Expression
1 cfilfval D ∞Met X CauFil D = f Fil X | x + y f D y × y 0 x
2 1 eleq2d D ∞Met X F CauFil D F f Fil X | x + y f D y × y 0 x
3 rexeq f = F y f D y × y 0 x y F D y × y 0 x
4 3 ralbidv f = F x + y f D y × y 0 x x + y F D y × y 0 x
5 4 elrab F f Fil X | x + y f D y × y 0 x F Fil X x + y F D y × y 0 x
6 2 5 bitrdi D ∞Met X F CauFil D F Fil X x + y F D y × y 0 x