Metamath Proof Explorer


Theorem caufval

Description: The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Assertion caufval D ∞Met X Cau D = f X 𝑝𝑚 | x + k f k : k f k ball D x

Proof

Step Hyp Ref Expression
1 df-cau Cau = d ran ∞Met f dom dom d 𝑝𝑚 | x + k f k : k f k ball d x
2 dmeq d = D dom d = dom D
3 2 dmeqd d = D dom dom d = dom dom D
4 xmetf D ∞Met X D : X × X *
5 4 fdmd D ∞Met X dom D = X × X
6 5 dmeqd D ∞Met X dom dom D = dom X × X
7 dmxpid dom X × X = X
8 6 7 eqtrdi D ∞Met X dom dom D = X
9 3 8 sylan9eqr D ∞Met X d = D dom dom d = X
10 9 oveq1d D ∞Met X d = D dom dom d 𝑝𝑚 = X 𝑝𝑚
11 simpr D ∞Met X d = D d = D
12 11 fveq2d D ∞Met X d = D ball d = ball D
13 12 oveqd D ∞Met X d = D f k ball d x = f k ball D x
14 13 feq3d D ∞Met X d = D f k : k f k ball d x f k : k f k ball D x
15 14 rexbidv D ∞Met X d = D k f k : k f k ball d x k f k : k f k ball D x
16 15 ralbidv D ∞Met X d = D x + k f k : k f k ball d x x + k f k : k f k ball D x
17 10 16 rabeqbidv D ∞Met X d = D f dom dom d 𝑝𝑚 | x + k f k : k f k ball d x = f X 𝑝𝑚 | x + k f k : k f k ball D x
18 fvssunirn ∞Met X ran ∞Met
19 18 sseli D ∞Met X D ran ∞Met
20 ovex X 𝑝𝑚 V
21 20 rabex f X 𝑝𝑚 | x + k f k : k f k ball D x V
22 21 a1i D ∞Met X f X 𝑝𝑚 | x + k f k : k f k ball D x V
23 1 17 19 22 fvmptd2 D ∞Met X Cau D = f X 𝑝𝑚 | x + k f k : k f k ball D x