Metamath Proof Explorer

Theorem iscau2

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, 14-Nov-2013)

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 iscau 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( F ` j ) ( ball ` D ) x ) ) ) )
2 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
3 cnex 
 |-  CC e. _V
4 elpmg 
 |-  ( ( X e. dom *Met /\ CC e. _V ) -> ( F e. ( X ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. X ) ) ) )
5 2 3 4 sylancl 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( X ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. X ) ) ) )
6 5 simprbda 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( X ^pm CC ) ) -> Fun F )
7 ffvresb 
 |-  ( Fun F -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( F ` j ) ( ball ` D ) x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) ) )
8 6 7 syl 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( X ^pm CC ) ) -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( F ` j ) ( ball ` D ) x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) ) )
9 8 rexbidv 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( X ^pm CC ) ) -> ( E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( F ` j ) ( ball ` D ) x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) ) )
10 9 adantr 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( X ^pm CC ) ) /\ x e. RR+ ) -> ( E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( F ` j ) ( ball ` D ) x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) ) )
11 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
12 11 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. RR+ ) /\ j e. ZZ ) -> j e. ( ZZ>= ` j ) )
13 eleq1w 
 |-  ( k = j -> ( k e. dom F <-> j e. dom F ) )
14 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
15 14 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) <-> ( F ` j ) e. ( ( F ` j ) ( ball ` D ) x ) ) )
16 13 15 anbi12d 
 |-  ( k = j -> ( ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> ( j e. dom F /\ ( F ` j ) e. ( ( F ` j ) ( ball ` D ) x ) ) ) )
17 16 rspcv 
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) -> ( j e. dom F /\ ( F ` j ) e. ( ( F ` j ) ( ball ` D ) x ) ) ) )
18 12 17 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. RR+ ) /\ j e. ZZ ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) -> ( j e. dom F /\ ( F ` j ) e. ( ( F ` j ) ( ball ` D ) x ) ) ) )
19 n0i 
 |-  ( ( F ` j ) e. ( ( F ` j ) ( ball ` D ) x ) -> -. ( ( F ` j ) ( ball ` D ) x ) = (/) )
20 blf 
 |-  ( D e. ( *Met ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )
21 20 fdmd 
 |-  ( D e. ( *Met ` X ) -> dom ( ball ` D ) = ( X X. RR* ) )
22 ndmovg 
 |-  ( ( dom ( ball ` D ) = ( X X. RR* ) /\ -. ( ( F ` j ) e. X /\ x e. RR* ) ) -> ( ( F ` j ) ( ball ` D ) x ) = (/) )
23 22 ex 
 |-  ( dom ( ball ` D ) = ( X X. RR* ) -> ( -. ( ( F ` j ) e. X /\ x e. RR* ) -> ( ( F ` j ) ( ball ` D ) x ) = (/) ) )
24 21 23 syl 
 |-  ( D e. ( *Met ` X ) -> ( -. ( ( F ` j ) e. X /\ x e. RR* ) -> ( ( F ` j ) ( ball ` D ) x ) = (/) ) )
25 24 con1d 
 |-  ( D e. ( *Met ` X ) -> ( -. ( ( F ` j ) ( ball ` D ) x ) = (/) -> ( ( F ` j ) e. X /\ x e. RR* ) ) )
26 simpl 
 |-  ( ( ( F ` j ) e. X /\ x e. RR* ) -> ( F ` j ) e. X )
27 19 25 26 syl56 
 |-  ( D e. ( *Met ` X ) -> ( ( F ` j ) e. ( ( F ` j ) ( ball ` D ) x ) -> ( F ` j ) e. X ) )
28 27 adantld 
 |-  ( D e. ( *Met ` X ) -> ( ( j e. dom F /\ ( F ` j ) e. ( ( F ` j ) ( ball ` D ) x ) ) -> ( F ` j ) e. X ) )
29 28 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. RR+ ) /\ j e. ZZ ) -> ( ( j e. dom F /\ ( F ` j ) e. ( ( F ` j ) ( ball ` D ) x ) ) -> ( F ` j ) e. X ) )
30 18 29 syld 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. RR+ ) /\ j e. ZZ ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) -> ( F ` j ) e. X ) )
31 14 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. X <-> ( F ` j ) e. X ) )
32 14 oveq1d 
 |-  ( k = j -> ( ( F ` k ) D ( F ` j ) ) = ( ( F ` j ) D ( F ` j ) ) )
33 32 breq1d 
 |-  ( k = j -> ( ( ( F ` k ) D ( F ` j ) ) < x <-> ( ( F ` j ) D ( F ` j ) ) < x ) )
34 13 31 33 3anbi123d 
 |-  ( k = j -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( j e. dom F /\ ( F ` j ) e. X /\ ( ( F ` j ) D ( F ` j ) ) < x ) ) )
35 34 rspcv 
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> ( j e. dom F /\ ( F ` j ) e. X /\ ( ( F ` j ) D ( F ` j ) ) < x ) ) )
36 12 35 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. RR+ ) /\ j e. ZZ ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> ( j e. dom F /\ ( F ` j ) e. X /\ ( ( F ` j ) D ( F ` j ) ) < x ) ) )
37 simp2 
 |-  ( ( j e. dom F /\ ( F ` j ) e. X /\ ( ( F ` j ) D ( F ` j ) ) < x ) -> ( F ` j ) e. X )
38 36 37 syl6 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. RR+ ) /\ j e. ZZ ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> ( F ` j ) e. X ) )
39 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
40 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ x e. RR* ) -> ( ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) <-> ( ( F ` k ) e. X /\ ( ( F ` j ) D ( F ` k ) ) < x ) ) )
41 39 40 syl3an3 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ x e. RR+ ) -> ( ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) <-> ( ( F ` k ) e. X /\ ( ( F ` j ) D ( F ` k ) ) < x ) ) )
42 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ ( F ` k ) e. X ) -> ( ( F ` j ) D ( F ` k ) ) = ( ( F ` k ) D ( F ` j ) ) )
43 42 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X ) /\ ( F ` k ) e. X ) -> ( ( F ` j ) D ( F ` k ) ) = ( ( F ` k ) D ( F ` j ) ) )
44 43 3adantl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ x e. RR+ ) /\ ( F ` k ) e. X ) -> ( ( F ` j ) D ( F ` k ) ) = ( ( F ` k ) D ( F ` j ) ) )
45 44 breq1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ x e. RR+ ) /\ ( F ` k ) e. X ) -> ( ( ( F ` j ) D ( F ` k ) ) < x <-> ( ( F ` k ) D ( F ` j ) ) < x ) )
46 45 pm5.32da 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ x e. RR+ ) -> ( ( ( F ` k ) e. X /\ ( ( F ` j ) D ( F ` k ) ) < x ) <-> ( ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
47 41 46 bitrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ x e. RR+ ) -> ( ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) <-> ( ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
48 47 3com23 
 |-  ( ( D e. ( *Met ` X ) /\ x e. RR+ /\ ( F ` j ) e. X ) -> ( ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) <-> ( ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
49 48 anbi2d 
 |-  ( ( D e. ( *Met ` X ) /\ x e. RR+ /\ ( F ` j ) e. X ) -> ( ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> ( k e. dom F /\ ( ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
50 3anass 
 |-  ( ( 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 ) ) )
51 49 50 bitr4di 
 |-  ( ( D e. ( *Met ` X ) /\ x e. RR+ /\ ( F ` j ) e. X ) -> ( ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
52 51 ralbidv 
 |-  ( ( D e. ( *Met ` X ) /\ x e. RR+ /\ ( F ` j ) e. X ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
53 52 3expia 
 |-  ( ( D e. ( *Met ` X ) /\ x e. RR+ ) -> ( ( F ` j ) e. X -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
54 53 adantr 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. RR+ ) /\ j e. ZZ ) -> ( ( F ` j ) e. X -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
55 30 38 54 pm5.21ndd 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. RR+ ) /\ j e. ZZ ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
56 55 rexbidva 
 |-  ( ( D e. ( *Met ` X ) /\ x e. RR+ ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
57 56 adantlr 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( X ^pm CC ) ) /\ x e. RR+ ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( F ` j ) ( ball ` D ) x ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
58 10 57 bitrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( X ^pm CC ) ) /\ x e. RR+ ) -> ( E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( F ` j ) ( ball ` D ) x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )
59 58 ralbidva 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( X ^pm CC ) ) -> ( A. x e. RR+ E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( F ` j ) ( ball ` D ) 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 ) ) )
60 59 pm5.32da 
 |-  ( D e. ( *Met ` X ) -> ( ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( F ` j ) ( ball ` D ) 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 ) ) ) )
61 1 60 bitrd 
 |-  ( 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 ) ) ) )