Metamath Proof Explorer

Theorem causs

Description: Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008) (Revised by Mario Carneiro, 30-Dec-2013)

Ref Expression
Assertion causs 
|- ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) -> ( F e. ( Cau ` D ) <-> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 caufpm 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> F e. ( X ^pm CC ) )
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 biimpa 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( X ^pm CC ) ) -> ( Fun F /\ F C_ ( CC X. X ) ) )
7 1 6 syldan 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> ( Fun F /\ F C_ ( CC X. X ) ) )
8 rnss 
 |-  ( F C_ ( CC X. X ) -> ran F C_ ran ( CC X. X ) )
9 7 8 simpl2im 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> ran F C_ ran ( CC X. X ) )
10 rnxpss 
 |-  ran ( CC X. X ) C_ X
11 9 10 sstrdi 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> ran F C_ X )
12 11 adantlr 
 |-  ( ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) /\ F e. ( Cau ` D ) ) -> ran F C_ X )
13 frn 
 |-  ( F : NN --> Y -> ran F C_ Y )
14 13 ad2antlr 
 |-  ( ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) /\ F e. ( Cau ` D ) ) -> ran F C_ Y )
15 12 14 ssind 
 |-  ( ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) /\ F e. ( Cau ` D ) ) -> ran F C_ ( X i^i Y ) )
16 15 ex 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) -> ( F e. ( Cau ` D ) -> ran F C_ ( X i^i Y ) ) )
17 xmetres 
 |-  ( D e. ( *Met ` X ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) )
18 caufpm 
 |-  ( ( ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) /\ F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) -> F e. ( ( X i^i Y ) ^pm CC ) )
19 17 18 sylan 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) -> F e. ( ( X i^i Y ) ^pm CC ) )
20 inex1g 
 |-  ( X e. dom *Met -> ( X i^i Y ) e. _V )
21 2 20 syl 
 |-  ( D e. ( *Met ` X ) -> ( X i^i Y ) e. _V )
22 elpmg 
 |-  ( ( ( X i^i Y ) e. _V /\ CC e. _V ) -> ( F e. ( ( X i^i Y ) ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. ( X i^i Y ) ) ) ) )
23 21 3 22 sylancl 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( ( X i^i Y ) ^pm CC ) <-> ( Fun F /\ F C_ ( CC X. ( X i^i Y ) ) ) ) )
24 23 biimpa 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( ( X i^i Y ) ^pm CC ) ) -> ( Fun F /\ F C_ ( CC X. ( X i^i Y ) ) ) )
25 19 24 syldan 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) -> ( Fun F /\ F C_ ( CC X. ( X i^i Y ) ) ) )
26 rnss 
 |-  ( F C_ ( CC X. ( X i^i Y ) ) -> ran F C_ ran ( CC X. ( X i^i Y ) ) )
27 25 26 simpl2im 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) -> ran F C_ ran ( CC X. ( X i^i Y ) ) )
28 rnxpss 
 |-  ran ( CC X. ( X i^i Y ) ) C_ ( X i^i Y )
29 27 28 sstrdi 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) -> ran F C_ ( X i^i Y ) )
30 29 ex 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` ( D |` ( Y X. Y ) ) ) -> ran F C_ ( X i^i Y ) ) )
31 30 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) -> ( F e. ( Cau ` ( D |` ( Y X. Y ) ) ) -> ran F C_ ( X i^i Y ) ) )
32 ffn 
 |-  ( F : NN --> Y -> F Fn NN )
33 df-f 
 |-  ( F : NN --> ( X i^i Y ) <-> ( F Fn NN /\ ran F C_ ( X i^i Y ) ) )
34 33 simplbi2 
 |-  ( F Fn NN -> ( ran F C_ ( X i^i Y ) -> F : NN --> ( X i^i Y ) ) )
35 32 34 syl 
 |-  ( F : NN --> Y -> ( ran F C_ ( X i^i Y ) -> F : NN --> ( X i^i Y ) ) )
36 inss2 
 |-  ( X i^i Y ) C_ Y
37 36 a1i 
 |-  ( D e. ( *Met ` X ) -> ( X i^i Y ) C_ Y )
38 fss 
 |-  ( ( F : NN --> ( X i^i Y ) /\ ( X i^i Y ) C_ Y ) -> F : NN --> Y )
39 37 38 sylan2 
 |-  ( ( F : NN --> ( X i^i Y ) /\ D e. ( *Met ` X ) ) -> F : NN --> Y )
40 39 ancoms 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> F : NN --> Y )
41 ffvelrn 
 |-  ( ( F : NN --> Y /\ y e. NN ) -> ( F ` y ) e. Y )
42 41 adantr 
 |-  ( ( ( F : NN --> Y /\ y e. NN ) /\ z e. ( ZZ>= ` y ) ) -> ( F ` y ) e. Y )
43 eluznn 
 |-  ( ( y e. NN /\ z e. ( ZZ>= ` y ) ) -> z e. NN )
44 ffvelrn 
 |-  ( ( F : NN --> Y /\ z e. NN ) -> ( F ` z ) e. Y )
45 43 44 sylan2 
 |-  ( ( F : NN --> Y /\ ( y e. NN /\ z e. ( ZZ>= ` y ) ) ) -> ( F ` z ) e. Y )
46 45 anassrs 
 |-  ( ( ( F : NN --> Y /\ y e. NN ) /\ z e. ( ZZ>= ` y ) ) -> ( F ` z ) e. Y )
47 42 46 ovresd 
 |-  ( ( ( F : NN --> Y /\ y e. NN ) /\ z e. ( ZZ>= ` y ) ) -> ( ( F ` y ) ( D |` ( Y X. Y ) ) ( F ` z ) ) = ( ( F ` y ) D ( F ` z ) ) )
48 47 breq1d 
 |-  ( ( ( F : NN --> Y /\ y e. NN ) /\ z e. ( ZZ>= ` y ) ) -> ( ( ( F ` y ) ( D |` ( Y X. Y ) ) ( F ` z ) ) < x <-> ( ( F ` y ) D ( F ` z ) ) < x ) )
49 48 ralbidva 
 |-  ( ( F : NN --> Y /\ y e. NN ) -> ( A. z e. ( ZZ>= ` y ) ( ( F ` y ) ( D |` ( Y X. Y ) ) ( F ` z ) ) < x <-> A. z e. ( ZZ>= ` y ) ( ( F ` y ) D ( F ` z ) ) < x ) )
50 49 rexbidva 
 |-  ( F : NN --> Y -> ( E. y e. NN A. z e. ( ZZ>= ` y ) ( ( F ` y ) ( D |` ( Y X. Y ) ) ( F ` z ) ) < x <-> E. y e. NN A. z e. ( ZZ>= ` y ) ( ( F ` y ) D ( F ` z ) ) < x ) )
51 50 ralbidv 
 |-  ( F : NN --> Y -> ( A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( ( F ` y ) ( D |` ( Y X. Y ) ) ( F ` z ) ) < x <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( ( F ` y ) D ( F ` z ) ) < x ) )
52 40 51 syl 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> ( A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( ( F ` y ) ( D |` ( Y X. Y ) ) ( F ` z ) ) < x <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( ( F ` y ) D ( F ` z ) ) < x ) )
53 nnuz 
 |-  NN = ( ZZ>= ` 1 )
54 17 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) )
55 1zzd 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> 1 e. ZZ )
56 eqidd 
 |-  ( ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) /\ z e. NN ) -> ( F ` z ) = ( F ` z ) )
57 eqidd 
 |-  ( ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) /\ y e. NN ) -> ( F ` y ) = ( F ` y ) )
58 simpr 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> F : NN --> ( X i^i Y ) )
59 53 54 55 56 57 58 iscauf 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> ( F e. ( Cau ` ( D |` ( Y X. Y ) ) ) <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( ( F ` y ) ( D |` ( Y X. Y ) ) ( F ` z ) ) < x ) )
60 simpl 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> D e. ( *Met ` X ) )
61 id 
 |-  ( F : NN --> ( X i^i Y ) -> F : NN --> ( X i^i Y ) )
62 inss1 
 |-  ( X i^i Y ) C_ X
63 62 a1i 
 |-  ( D e. ( *Met ` X ) -> ( X i^i Y ) C_ X )
64 fss 
 |-  ( ( F : NN --> ( X i^i Y ) /\ ( X i^i Y ) C_ X ) -> F : NN --> X )
65 61 63 64 syl2anr 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> F : NN --> X )
66 53 60 55 56 57 65 iscauf 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( ( F ` y ) D ( F ` z ) ) < x ) )
67 52 59 66 3bitr4rd 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> ( X i^i Y ) ) -> ( F e. ( Cau ` D ) <-> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) )
68 67 ex 
 |-  ( D e. ( *Met ` X ) -> ( F : NN --> ( X i^i Y ) -> ( F e. ( Cau ` D ) <-> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) ) )
69 35 68 sylan9r 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) -> ( ran F C_ ( X i^i Y ) -> ( F e. ( Cau ` D ) <-> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) ) )
70 16 31 69 pm5.21ndd 
 |-  ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) -> ( F e. ( Cau ` D ) <-> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) )