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 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∞MetXFCauDFX𝑝𝑚x+kFk:kFkballDx

Proof

Step Hyp Ref Expression
1 caufval D∞MetXCauD=fX𝑝𝑚|x+kfk:kfkballDx
2 1 eleq2d D∞MetXFCauDFfX𝑝𝑚|x+kfk:kfkballDx
3 reseq1 f=Ffk=Fk
4 eqidd f=Fk=k
5 fveq1 f=Ffk=Fk
6 5 oveq1d f=FfkballDx=FkballDx
7 3 4 6 feq123d f=Ffk:kfkballDxFk:kFkballDx
8 7 rexbidv f=Fkfk:kfkballDxkFk:kFkballDx
9 8 ralbidv f=Fx+kfk:kfkballDxx+kFk:kFkballDx
10 9 elrab FfX𝑝𝑚|x+kfk:kfkballDxFX𝑝𝑚x+kFk:kFkballDx
11 2 10 bitrdi D∞MetXFCauDFX𝑝𝑚x+kFk:kFkballDx