Metamath Proof Explorer

Theorem caucfil

Description: A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses caucfil.1 
|- Z = ( ZZ>= ` M )
caucfil.2 
|- L = ( ( X FilMap F ) ` ( ZZ>= " Z ) )
Assertion caucfil 
|- ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( F e. ( Cau ` D ) <-> L e. ( CauFil ` D ) ) )

Proof

Step Hyp Ref Expression
1 caucfil.1 
 |-  Z = ( ZZ>= ` M )
2 caucfil.2 
 |-  L = ( ( X FilMap F ) ` ( ZZ>= " Z ) )
3 df-3an 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
4 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
5 4 adantll 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
6 simpll3 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> F : Z --> X )
7 6 fdmd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> dom F = Z )
8 5 7 eleqtrrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. dom F )
9 6 5 ffvelcdmd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. X )
10 8 9 jca 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( k e. dom F /\ ( F ` k ) e. X ) )
11 10 biantrurd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x <-> ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
12 uzss 
 |-  ( k e. ( ZZ>= ` j ) -> ( ZZ>= ` k ) C_ ( ZZ>= ` j ) )
13 12 adantl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ZZ>= ` k ) C_ ( ZZ>= ` j ) )
14 13 sseld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( m e. ( ZZ>= ` k ) -> m e. ( ZZ>= ` j ) ) )
15 14 pm4.71rd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( m e. ( ZZ>= ` k ) <-> ( m e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` k ) ) ) )
16 15 imbi1d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) <-> ( ( m e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` k ) ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
17 impexp 
 |-  ( ( ( m e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` k ) ) -> ( ( F ` k ) D ( F ` m ) ) < x ) <-> ( m e. ( ZZ>= ` j ) -> ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
18 16 17 bitrdi 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) <-> ( m e. ( ZZ>= ` j ) -> ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) ) )
19 18 ralbidv2 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x <-> A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
20 11 19 bitr3d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
21 3 20 bitrid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
22 21 ralbidva 
 |-  ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
23 r19.26-2 
 |-  ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) ) <-> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) ) )
24 eleq1w 
 |-  ( u = k -> ( u e. ( ZZ>= ` m ) <-> k e. ( ZZ>= ` m ) ) )
25 fveq2 
 |-  ( u = k -> ( F ` u ) = ( F ` k ) )
26 25 oveq2d 
 |-  ( u = k -> ( ( F ` m ) D ( F ` u ) ) = ( ( F ` m ) D ( F ` k ) ) )
27 26 breq1d 
 |-  ( u = k -> ( ( ( F ` m ) D ( F ` u ) ) < x <-> ( ( F ` m ) D ( F ` k ) ) < x ) )
28 24 27 imbi12d 
 |-  ( u = k -> ( ( u e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` u ) ) < x ) <-> ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) ) )
29 28 cbvralvw 
 |-  ( A. u e. ( ZZ>= ` j ) ( u e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` u ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) )
30 29 ralbii 
 |-  ( A. m e. ( ZZ>= ` j ) A. u e. ( ZZ>= ` j ) ( u e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` u ) ) < x ) <-> A. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` j ) ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) )
31 fveq2 
 |-  ( m = k -> ( ZZ>= ` m ) = ( ZZ>= ` k ) )
32 31 eleq2d 
 |-  ( m = k -> ( u e. ( ZZ>= ` m ) <-> u e. ( ZZ>= ` k ) ) )
33 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
34 33 oveq1d 
 |-  ( m = k -> ( ( F ` m ) D ( F ` u ) ) = ( ( F ` k ) D ( F ` u ) ) )
35 34 breq1d 
 |-  ( m = k -> ( ( ( F ` m ) D ( F ` u ) ) < x <-> ( ( F ` k ) D ( F ` u ) ) < x ) )
36 32 35 imbi12d 
 |-  ( m = k -> ( ( u e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` u ) ) < x ) <-> ( u e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` u ) ) < x ) ) )
37 eleq1w 
 |-  ( u = m -> ( u e. ( ZZ>= ` k ) <-> m e. ( ZZ>= ` k ) ) )
38 fveq2 
 |-  ( u = m -> ( F ` u ) = ( F ` m ) )
39 38 oveq2d 
 |-  ( u = m -> ( ( F ` k ) D ( F ` u ) ) = ( ( F ` k ) D ( F ` m ) ) )
40 39 breq1d 
 |-  ( u = m -> ( ( ( F ` k ) D ( F ` u ) ) < x <-> ( ( F ` k ) D ( F ` m ) ) < x ) )
41 37 40 imbi12d 
 |-  ( u = m -> ( ( u e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` u ) ) < x ) <-> ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
42 36 41 cbvral2vw 
 |-  ( A. m e. ( ZZ>= ` j ) A. u e. ( ZZ>= ` j ) ( u e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` u ) ) < x ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) )
43 ralcom 
 |-  ( A. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` j ) ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) )
44 30 42 43 3bitr3i 
 |-  ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) )
45 44 anbi2i 
 |-  ( ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) <-> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) ) )
46 anidm 
 |-  ( ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) )
47 23 45 46 3bitr2i 
 |-  ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) )
48 simpll1 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> D e. ( *Met ` X ) )
49 simpll3 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> F : Z --> X )
50 1 uztrn2 
 |-  ( ( j e. Z /\ m e. ( ZZ>= ` j ) ) -> m e. Z )
51 50 ad2ant2l 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> m e. Z )
52 49 51 ffvelcdmd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( F ` m ) e. X )
53 9 adantrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. X )
54 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` m ) e. X /\ ( F ` k ) e. X ) -> ( ( F ` m ) D ( F ` k ) ) = ( ( F ` k ) D ( F ` m ) ) )
55 48 52 53 54 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( ( F ` m ) D ( F ` k ) ) = ( ( F ` k ) D ( F ` m ) ) )
56 55 breq1d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( ( ( F ` m ) D ( F ` k ) ) < x <-> ( ( F ` k ) D ( F ` m ) ) < x ) )
57 56 imbi2d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) <-> ( k e. ( ZZ>= ` m ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
58 57 anbi2d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) ) <-> ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ ( k e. ( ZZ>= ` m ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) ) )
59 jaob 
 |-  ( ( ( m e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` m ) ) -> ( ( F ` k ) D ( F ` m ) ) < x ) <-> ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ ( k e. ( ZZ>= ` m ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) )
60 eluzelz 
 |-  ( k e. ( ZZ>= ` j ) -> k e. ZZ )
61 eluzelz 
 |-  ( m e. ( ZZ>= ` j ) -> m e. ZZ )
62 uztric 
 |-  ( ( k e. ZZ /\ m e. ZZ ) -> ( m e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` m ) ) )
63 60 61 62 syl2an 
 |-  ( ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) -> ( m e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` m ) ) )
64 63 adantl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( m e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` m ) ) )
65 pm5.5 
 |-  ( ( m e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` m ) ) -> ( ( ( m e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` m ) ) -> ( ( F ` k ) D ( F ` m ) ) < x ) <-> ( ( F ` k ) D ( F ` m ) ) < x ) )
66 64 65 syl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( ( ( m e. ( ZZ>= ` k ) \/ k e. ( ZZ>= ` m ) ) -> ( ( F ` k ) D ( F ` m ) ) < x ) <-> ( ( F ` k ) D ( F ` m ) ) < x ) )
67 59 66 bitr3id 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ ( k e. ( ZZ>= ` m ) -> ( ( F ` k ) D ( F ` m ) ) < x ) ) <-> ( ( F ` k ) D ( F ` m ) ) < x ) )
68 58 67 bitrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) /\ ( k e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` j ) ) ) -> ( ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) ) <-> ( ( F ` k ) D ( F ` m ) ) < x ) )
69 68 2ralbidva 
 |-  ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) /\ ( k e. ( ZZ>= ` m ) -> ( ( F ` m ) D ( F ` k ) ) < x ) ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` m ) ) < x ) )
70 47 69 bitr3id 
 |-  ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( m e. ( ZZ>= ` k ) -> ( ( F ` k ) D ( F ` m ) ) < x ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` m ) ) < x ) )
71 22 70 bitrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` m ) ) < x ) )
72 71 rexbidva 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` m ) ) < x ) )
73 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
74 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
75 73 74 ax-mp 
 |-  ZZ>= Fn ZZ
76 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
77 1 76 eqsstri 
 |-  Z C_ ZZ
78 raleq 
 |-  ( u = ( ZZ>= ` j ) -> ( A. m e. u ( ( F ` k ) D ( F ` m ) ) < x <-> A. m e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` m ) ) < x ) )
79 78 raleqbi1dv 
 |-  ( u = ( ZZ>= ` j ) -> ( A. k e. u A. m e. u ( ( F ` k ) D ( F ` m ) ) < x <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` m ) ) < x ) )
80 79 rexima 
 |-  ( ( ZZ>= Fn ZZ /\ Z C_ ZZ ) -> ( E. u e. ( ZZ>= " Z ) A. k e. u A. m e. u ( ( F ` k ) D ( F ` m ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` m ) ) < x ) )
81 75 77 80 mp2an 
 |-  ( E. u e. ( ZZ>= " Z ) A. k e. u A. m e. u ( ( F ` k ) D ( F ` m ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` m ) ) < x )
82 72 81 bitr4di 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> E. u e. ( ZZ>= " Z ) A. k e. u A. m e. u ( ( F ` k ) D ( F ` m ) ) < x ) )
83 82 ralbidv 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> A. x e. RR+ E. u e. ( ZZ>= " Z ) A. k e. u A. m e. u ( ( F ` k ) D ( F ` m ) ) < x ) )
84 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
85 84 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ ) -> X e. dom *Met )
86 cnex 
 |-  CC e. _V
87 85 86 jctir 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ ) -> ( X e. dom *Met /\ CC e. _V ) )
88 zsscn 
 |-  ZZ C_ CC
89 77 88 sstri 
 |-  Z C_ CC
90 89 jctr 
 |-  ( F : Z --> X -> ( F : Z --> X /\ Z C_ CC ) )
91 elpm2r 
 |-  ( ( ( X e. dom *Met /\ CC e. _V ) /\ ( F : Z --> X /\ Z C_ CC ) ) -> F e. ( X ^pm CC ) )
92 87 90 91 syl2an 
 |-  ( ( ( D e. ( *Met ` X ) /\ M e. ZZ ) /\ F : Z --> X ) -> F e. ( X ^pm CC ) )
93 simpl 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ ) -> D e. ( *Met ` X ) )
94 simpr 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ ) -> M e. ZZ )
95 1 93 94 iscau3 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ ) -> ( 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 /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) ) )
96 95 baibd 
 |-  ( ( ( D e. ( *Met ` X ) /\ M e. ZZ ) /\ F e. ( X ^pm CC ) ) -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
97 92 96 syldan 
 |-  ( ( ( D e. ( *Met ` X ) /\ M e. ZZ ) /\ F : Z --> X ) -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
98 97 3impa 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
99 2 eleq1i 
 |-  ( L e. ( CauFil ` D ) <-> ( ( X FilMap F ) ` ( ZZ>= " Z ) ) e. ( CauFil ` D ) )
100 1 uzfbas 
 |-  ( M e. ZZ -> ( ZZ>= " Z ) e. ( fBas ` Z ) )
101 fmcfil 
 |-  ( ( D e. ( *Met ` X ) /\ ( ZZ>= " Z ) e. ( fBas ` Z ) /\ F : Z --> X ) -> ( ( ( X FilMap F ) ` ( ZZ>= " Z ) ) e. ( CauFil ` D ) <-> A. x e. RR+ E. u e. ( ZZ>= " Z ) A. k e. u A. m e. u ( ( F ` k ) D ( F ` m ) ) < x ) )
102 100 101 syl3an2 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( ( ( X FilMap F ) ` ( ZZ>= " Z ) ) e. ( CauFil ` D ) <-> A. x e. RR+ E. u e. ( ZZ>= " Z ) A. k e. u A. m e. u ( ( F ` k ) D ( F ` m ) ) < x ) )
103 99 102 bitrid 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( L e. ( CauFil ` D ) <-> A. x e. RR+ E. u e. ( ZZ>= " Z ) A. k e. u A. m e. u ( ( F ` k ) D ( F ` m ) ) < x ) )
104 83 98 103 3bitr4d 
 |-  ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( F e. ( Cau ` D ) <-> L e. ( CauFil ` D ) ) )