This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscau4

Description: Express the property " F is a Cauchy sequence of metric D " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006) (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 )
Assertion 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 ) ) ) )

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 1 2 3 iscau3 
 |-  ( 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 /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) ) )
7 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
8 7 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
9 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
10 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
11 8 9 10 3syl 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` j ) )
12 fveq2 
 |-  ( k = j -> ( ZZ>= ` k ) = ( ZZ>= ` j ) )
13 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
14 13 oveq1d 
 |-  ( k = j -> ( ( F ` k ) D ( F ` m ) ) = ( ( F ` j ) D ( F ` m ) ) )
15 14 breq1d 
 |-  ( k = j -> ( ( ( F ` k ) D ( F ` m ) ) < x <-> ( ( F ` j ) D ( F ` m ) ) < x ) )
16 12 15 raleqbidv 
 |-  ( k = j -> ( A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x <-> A. m e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` m ) ) < x ) )
17 16 rspcv 
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x -> A. m e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` m ) ) < x ) )
18 11 17 syl 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x -> A. m e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` m ) ) < x ) )
19 18 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x -> A. m e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` m ) ) < x ) )
20 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
21 20 oveq2d 
 |-  ( m = k -> ( ( F ` j ) D ( F ` m ) ) = ( ( F ` j ) D ( F ` k ) ) )
22 21 breq1d 
 |-  ( m = k -> ( ( ( F ` j ) D ( F ` m ) ) < x <-> ( ( F ` j ) D ( F ` k ) ) < x ) )
23 22 cbvralvw 
 |-  ( A. m e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` m ) ) < x <-> A. k e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` k ) ) < x )
24 simpr 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X ) -> ( F ` k ) e. X )
25 24 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. X )
26 13 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. X <-> ( F ` j ) e. X ) )
27 26 rspcv 
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. X -> ( F ` j ) e. X ) )
28 11 25 27 syl2im 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) -> ( F ` j ) e. X ) )
29 28 imp 
 |-  ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( F ` j ) e. X )
30 r19.26 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` j ) D ( F ` k ) ) < x ) <-> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` k ) ) < x ) )
31 2 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) /\ ( k e. dom F /\ ( F ` k ) e. X ) ) -> D e. ( *Met ` X ) )
32 simplr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) /\ ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( F ` j ) e. X )
33 simprr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) /\ ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( F ` k ) e. X )
34 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ ( F ` k ) e. X ) -> ( ( F ` j ) D ( F ` k ) ) = ( ( F ` k ) D ( F ` j ) ) )
35 31 32 33 34 syl3anc 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) /\ ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( ( F ` j ) D ( F ` k ) ) = ( ( F ` k ) D ( F ` j ) ) )
36 35 breq1d 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) /\ ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( ( ( F ` j ) D ( F ` k ) ) < x <-> ( ( F ` k ) D ( F ` j ) ) < x ) )
37 36 biimpd 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) /\ ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( ( ( F ` j ) D ( F ` k ) ) < x -> ( ( F ` k ) D ( F ` j ) ) < x ) )
38 37 expimpd 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) -> ( ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` j ) D ( F ` k ) ) < x ) -> ( ( F ` k ) D ( F ` j ) ) < x ) )
39 38 ralimdv 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) -> ( A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` j ) D ( F ` k ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) )
40 30 39 biimtrrid 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) -> ( ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` k ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) )
41 40 expd 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F ` j ) e. X ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` k ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) ) )
42 41 impancom 
 |-  ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( ( F ` j ) e. X -> ( A. k e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` k ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) ) )
43 29 42 mpd 
 |-  ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` k ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) )
44 23 43 biimtrid 
 |-  ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( A. m e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` m ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) )
45 19 44 syld 
 |-  ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) ) -> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) )
46 45 imdistanda 
 |-  ( ( ph /\ j e. Z ) -> ( ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) /\ A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) ) )
47 r19.26 
 |-  ( 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 ) ( k e. dom F /\ ( F ` k ) e. X ) /\ A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
48 r19.26 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) D ( F ` j ) ) < x ) )
49 46 47 48 3imtr4g 
 |-  ( ( ph /\ 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 ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
50 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 ) )
51 50 ralbii 
 |-  ( 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 ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
52 df-3an 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
53 52 ralbii 
 |-  ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
54 49 51 53 3imtr4g 
 |-  ( ( ph /\ 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 ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
55 54 reximdva 
 |-  ( ph -> ( 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 ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
56 55 ralimdv 
 |-  ( ph -> ( 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. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
57 56 anim2d 
 |-  ( ph -> ( ( 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 ) ) -> ( 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 /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
58 6 57 sylbid 
 |-  ( 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 /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
59 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
60 1 59 eqsstri 
 |-  Z C_ ZZ
61 ssrexv 
 |-  ( Z C_ ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
62 60 61 ax-mp 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
63 62 ralimi 
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
64 63 anim2i 
 |-  ( ( 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 /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) -> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
65 iscau2 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
66 64 65 imbitrrid 
 |-  ( D e. ( *Met ` X ) -> ( ( 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 /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) -> F e. ( Cau ` D ) ) )
67 2 66 syl 
 |-  ( ph -> ( ( 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 /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) -> F e. ( Cau ` D ) ) )
68 58 67 impbid 
 |-  ( 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 /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
69 simpl 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> j e. Z )
70 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
71 69 70 jca 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( j e. Z /\ k e. Z ) )
72 4 adantrl 
 |-  ( ( ph /\ ( j e. Z /\ k e. Z ) ) -> ( F ` k ) = A )
73 72 eleq1d 
 |-  ( ( ph /\ ( j e. Z /\ k e. Z ) ) -> ( ( F ` k ) e. X <-> A e. X ) )
74 5 adantrr 
 |-  ( ( ph /\ ( j e. Z /\ k e. Z ) ) -> ( F ` j ) = B )
75 72 74 oveq12d 
 |-  ( ( ph /\ ( j e. Z /\ k e. Z ) ) -> ( ( F ` k ) D ( F ` j ) ) = ( A D B ) )
76 75 breq1d 
 |-  ( ( ph /\ ( j e. Z /\ k e. Z ) ) -> ( ( ( F ` k ) D ( F ` j ) ) < x <-> ( A D B ) < x ) )
77 73 76 3anbi23d 
 |-  ( ( ph /\ ( j e. Z /\ k e. Z ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
78 71 77 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
79 78 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
80 79 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
81 80 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) )
82 81 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < 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 ) ) )
83 82 anbi2d 
 |-  ( ph -> ( ( 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 /\ ( ( F ` k ) D ( F ` j ) ) < 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 ) ) ) )
84 68 83 bitrd 
 |-  ( 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 ) ) ) )