Metamath Proof Explorer

Theorem iscauf

Description: Express the property " F is a Cauchy sequence of metric D " presupposing F is a function. (Contributed by NM, 24-Jul-2007) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses iscau3.2 
|- Z = ( ZZ>= ` M )
iscau3.3 
|- ( ph -> D e. ( *Met ` X ) )
iscau3.4 
|- ( ph -> M e. ZZ )
iscau4.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
iscau4.6 
|- ( ( ph /\ j e. Z ) -> ( F ` j ) = B )
iscauf.7 
|- ( ph -> F : Z --> X )
Assertion iscauf 
|- ( ph -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B D A ) < x ) )

Proof

Step Hyp Ref Expression
1 iscau3.2 
 |-  Z = ( ZZ>= ` M )
2 iscau3.3 
 |-  ( ph -> D e. ( *Met ` X ) )
3 iscau3.4 
 |-  ( ph -> M e. ZZ )
4 iscau4.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5 iscau4.6 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) = B )
6 iscauf.7 
 |-  ( ph -> F : Z --> X )
7 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
8 2 7 syl 
 |-  ( ph -> X e. dom *Met )
9 cnex 
 |-  CC e. _V
10 8 9 jctir 
 |-  ( ph -> ( X e. dom *Met /\ CC e. _V ) )
11 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
12 zsscn 
 |-  ZZ C_ CC
13 11 12 sstri 
 |-  ( ZZ>= ` M ) C_ CC
14 1 13 eqsstri 
 |-  Z C_ CC
15 6 14 jctir 
 |-  ( ph -> ( F : Z --> X /\ Z C_ CC ) )
16 elpm2r 
 |-  ( ( ( X e. dom *Met /\ CC e. _V ) /\ ( F : Z --> X /\ Z C_ CC ) ) -> F e. ( X ^pm CC ) )
17 10 15 16 syl2anc 
 |-  ( ph -> F e. ( X ^pm CC ) )
18 17 biantrurd 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) ) )
19 2 adantr 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> D e. ( *Met ` X ) )
20 5 adantrr 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` j ) = B )
21 6 adantr 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> F : Z --> X )
22 simprl 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> j e. Z )
23 21 22 ffvelrnd 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` j ) e. X )
24 20 23 eqeltrrd 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> B e. X )
25 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
26 25 4 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) = A )
27 ffvelrn 
 |-  ( ( F : Z --> X /\ k e. Z ) -> ( F ` k ) e. X )
28 6 25 27 syl2an 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. X )
29 26 28 eqeltrrd 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> A e. X )
30 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ A e. X ) -> ( B D A ) = ( A D B ) )
31 19 24 29 30 syl3anc 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( B D A ) = ( A D B ) )
32 31 breq1d 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( B D A ) < x <-> ( A D B ) < x ) )
33 fdm 
 |-  ( F : Z --> X -> dom F = Z )
34 33 eleq2d 
 |-  ( F : Z --> X -> ( k e. dom F <-> k e. Z ) )
35 34 biimpar 
 |-  ( ( F : Z --> X /\ k e. Z ) -> k e. dom F )
36 6 25 35 syl2an 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> k e. dom F )
37 36 29 jca 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( k e. dom F /\ A e. X ) )
38 37 biantrurd 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( A D B ) < x <-> ( ( k e. dom F /\ A e. X ) /\ ( A D B ) < x ) ) )
39 df-3an 
 |-  ( ( k e. dom F /\ A e. X /\ ( A D B ) < x ) <-> ( ( k e. dom F /\ A e. X ) /\ ( A D B ) < x ) )
40 38 39 bitr4di 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( A D B ) < x <-> ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
41 32 40 bitrd 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( B D A ) < x <-> ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
42 41 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( B D A ) < x <-> ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
43 42 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( B D A ) < x <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
44 43 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( B D A ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
45 44 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B D A ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
46 1 2 3 4 5 iscau4 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) ) )
47 18 45 46 3bitr4rd 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B D A ) < x ) )