Metamath Proof Explorer


Theorem iscau

Description: Express the property " F is a Cauchy sequence of metric D ". Part of Definition 1.4-3 of Kreyszig p. 28. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion iscau D ∞Met X F Cau D F X 𝑝𝑚 x + k F k : k F k ball D x

Proof

Step Hyp Ref Expression
1 caufval D ∞Met X Cau D = f X 𝑝𝑚 | x + k f k : k f k ball D x
2 1 eleq2d D ∞Met X F Cau D F f X 𝑝𝑚 | x + k f k : k f k ball D x
3 reseq1 f = F f k = F k
4 eqidd f = F k = k
5 fveq1 f = F f k = F k
6 5 oveq1d f = F f k ball D x = F k ball D x
7 3 4 6 feq123d f = F f k : k f k ball D x F k : k F k ball D x
8 7 rexbidv f = F k f k : k f k ball D x k F k : k F k ball D x
9 8 ralbidv f = F x + k f k : k f k ball D x x + k F k : k F k ball D x
10 9 elrab F f X 𝑝𝑚 | x + k f k : k f k ball D x F X 𝑝𝑚 x + k F k : k F k ball D x
11 2 10 bitrdi D ∞Met X F Cau D F X 𝑝𝑚 x + k F k : k F k ball D x