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

Proof

Step Hyp Ref Expression
1 fvssunirn ∞Met X ran ∞Met
2 1 sseli D ∞Met X D 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 × y = D y × y
7 6 sseq1d d = D d y × y 0 x D y × y 0 x
8 7 rexbidv d = D y f d y × y 0 x y f D y × y 0 x
9 8 ralbidv d = D x + y f d y × y 0 x x + y f D y × y 0 x
10 5 9 rabeqbidv d = D f Fil dom dom d | x + y f d y × y 0 x = f Fil dom dom D | x + y f D y × y 0 x
11 df-cfil CauFil = d ran ∞Met f Fil dom dom d | x + y f d y × y 0 x
12 fvex Fil dom dom D V
13 12 rabex f Fil dom dom D | x + y f D y × y 0 x V
14 10 11 13 fvmpt D ran ∞Met CauFil D = f Fil dom dom D | x + y f D y × y 0 x
15 2 14 syl D ∞Met X CauFil D = f Fil dom dom D | x + y f D y × y 0 x
16 xmetdmdm D ∞Met X X = dom dom D
17 16 fveq2d D ∞Met X Fil X = Fil dom dom D
18 17 rabeqdv D ∞Met X f Fil X | x + y f D y × y 0 x = f Fil dom dom D | x + y f D y × y 0 x
19 15 18 eqtr4d D ∞Met X CauFil D = f Fil X | x + y f D y × y 0 x