Metamath Proof Explorer

Theorem caussi

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

Ref Expression
Assertion caussi 
|- ( D e. ( *Met ` X ) -> ( Cau ` ( D |` ( Y X. Y ) ) ) C_ ( Cau ` D ) )

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( X i^i Y ) C_ X
2 xpss2 
 |-  ( ( X i^i Y ) C_ X -> ( CC X. ( X i^i Y ) ) C_ ( CC X. X ) )
3 1 2 ax-mp 
 |-  ( CC X. ( X i^i Y ) ) C_ ( CC X. X )
4 sstr 
 |-  ( ( f C_ ( CC X. ( X i^i Y ) ) /\ ( CC X. ( X i^i Y ) ) C_ ( CC X. X ) ) -> f C_ ( CC X. X ) )
5 3 4 mpan2 
 |-  ( f C_ ( CC X. ( X i^i Y ) ) -> f C_ ( CC X. X ) )
6 5 anim2i 
 |-  ( ( Fun f /\ f C_ ( CC X. ( X i^i Y ) ) ) -> ( Fun f /\ f C_ ( CC X. X ) ) )
7 6 a1i 
 |-  ( D e. ( *Met ` X ) -> ( ( Fun f /\ f C_ ( CC X. ( X i^i Y ) ) ) -> ( Fun f /\ f C_ ( CC X. X ) ) ) )
8 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
9 inex1g 
 |-  ( X e. dom *Met -> ( X i^i Y ) e. _V )
10 8 9 syl 
 |-  ( D e. ( *Met ` X ) -> ( X i^i Y ) e. _V )
11 cnex 
 |-  CC e. _V
12 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 ) ) ) ) )
13 10 11 12 sylancl 
 |-  ( D e. ( *Met ` X ) -> ( f e. ( ( X i^i Y ) ^pm CC ) <-> ( Fun f /\ f C_ ( CC X. ( X i^i Y ) ) ) ) )
14 elpmg 
 |-  ( ( X e. dom *Met /\ CC e. _V ) -> ( f e. ( X ^pm CC ) <-> ( Fun f /\ f C_ ( CC X. X ) ) ) )
15 8 11 14 sylancl 
 |-  ( D e. ( *Met ` X ) -> ( f e. ( X ^pm CC ) <-> ( Fun f /\ f C_ ( CC X. X ) ) ) )
16 7 13 15 3imtr4d 
 |-  ( D e. ( *Met ` X ) -> ( f e. ( ( X i^i Y ) ^pm CC ) -> f e. ( X ^pm CC ) ) )
17 uzid 
 |-  ( y e. ZZ -> y e. ( ZZ>= ` y ) )
18 17 adantl 
 |-  ( ( D e. ( *Met ` X ) /\ y e. ZZ ) -> y e. ( ZZ>= ` y ) )
19 simp2 
 |-  ( ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> ( f ` z ) e. ( X i^i Y ) )
20 19 ralimi 
 |-  ( A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> A. z e. ( ZZ>= ` y ) ( f ` z ) e. ( X i^i Y ) )
21 fveq2 
 |-  ( z = y -> ( f ` z ) = ( f ` y ) )
22 21 eleq1d 
 |-  ( z = y -> ( ( f ` z ) e. ( X i^i Y ) <-> ( f ` y ) e. ( X i^i Y ) ) )
23 22 rspcva 
 |-  ( ( y e. ( ZZ>= ` y ) /\ A. z e. ( ZZ>= ` y ) ( f ` z ) e. ( X i^i Y ) ) -> ( f ` y ) e. ( X i^i Y ) )
24 18 20 23 syl2an 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) ) -> ( f ` y ) e. ( X i^i Y ) )
25 simpr 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. ( X i^i Y ) ) -> ( f ` y ) e. ( X i^i Y ) )
26 25 elin2d 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. ( X i^i Y ) ) -> ( f ` y ) e. Y )
27 inss2 
 |-  ( X i^i Y ) C_ Y
28 27 a1i 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) -> ( X i^i Y ) C_ Y )
29 28 sselda 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) /\ ( f ` z ) e. ( X i^i Y ) ) -> ( f ` z ) e. Y )
30 simplr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) /\ ( f ` z ) e. ( X i^i Y ) ) -> ( f ` y ) e. Y )
31 29 30 ovresd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) /\ ( f ` z ) e. ( X i^i Y ) ) -> ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) = ( ( f ` z ) D ( f ` y ) ) )
32 31 breq1d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) /\ ( f ` z ) e. ( X i^i Y ) ) -> ( ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x <-> ( ( f ` z ) D ( f ` y ) ) < x ) )
33 32 biimpd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) /\ ( f ` z ) e. ( X i^i Y ) ) -> ( ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x -> ( ( f ` z ) D ( f ` y ) ) < x ) )
34 33 imdistanda 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) -> ( ( ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> ( ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
35 1 a1i 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) -> ( X i^i Y ) C_ X )
36 35 sseld 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) -> ( ( f ` z ) e. ( X i^i Y ) -> ( f ` z ) e. X ) )
37 36 anim1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) -> ( ( ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) D ( f ` y ) ) < x ) -> ( ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
38 34 37 syld 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. Y ) -> ( ( ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> ( ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
39 26 38 syldan 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. ( X i^i Y ) ) -> ( ( ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> ( ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
40 39 anim2d 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. ( X i^i Y ) ) -> ( ( z e. dom f /\ ( ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) ) -> ( z e. dom f /\ ( ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) ) )
41 3anass 
 |-  ( ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) <-> ( z e. dom f /\ ( ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) ) )
42 3anass 
 |-  ( ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) <-> ( z e. dom f /\ ( ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
43 40 41 42 3imtr4g 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. ( X i^i Y ) ) -> ( ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
44 43 ralimdv 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ ( f ` y ) e. ( X i^i Y ) ) -> ( A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
45 44 impancom 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) ) -> ( ( f ` y ) e. ( X i^i Y ) -> A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
46 24 45 mpd 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. ZZ ) /\ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) ) -> A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) )
47 46 ex 
 |-  ( ( D e. ( *Met ` X ) /\ y e. ZZ ) -> ( A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
48 47 reximdva 
 |-  ( D e. ( *Met ` X ) -> ( E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
49 48 ralimdv 
 |-  ( D e. ( *Met ` X ) -> ( A. x e. RR+ E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) -> A. x e. RR+ E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) )
50 16 49 anim12d 
 |-  ( D e. ( *Met ` X ) -> ( ( f e. ( ( X i^i Y ) ^pm CC ) /\ A. x e. RR+ E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) ) -> ( f e. ( X ^pm CC ) /\ A. x e. RR+ E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) ) )
51 xmetres 
 |-  ( D e. ( *Met ` X ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) )
52 iscau2 
 |-  ( ( 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 ) /\ A. x e. RR+ E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) ) ) )
53 51 52 syl 
 |-  ( D e. ( *Met ` X ) -> ( f e. ( Cau ` ( D |` ( Y X. Y ) ) ) <-> ( f e. ( ( X i^i Y ) ^pm CC ) /\ A. x e. RR+ E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. ( X i^i Y ) /\ ( ( f ` z ) ( D |` ( Y X. Y ) ) ( f ` y ) ) < x ) ) ) )
54 iscau2 
 |-  ( D e. ( *Met ` X ) -> ( f e. ( Cau ` D ) <-> ( f e. ( X ^pm CC ) /\ A. x e. RR+ E. y e. ZZ A. z e. ( ZZ>= ` y ) ( z e. dom f /\ ( f ` z ) e. X /\ ( ( f ` z ) D ( f ` y ) ) < x ) ) ) )
55 50 53 54 3imtr4d 
 |-  ( D e. ( *Met ` X ) -> ( f e. ( Cau ` ( D |` ( Y X. Y ) ) ) -> f e. ( Cau ` D ) ) )
56 55 ssrdv 
 |-  ( D e. ( *Met ` X ) -> ( Cau ` ( D |` ( Y X. Y ) ) ) C_ ( Cau ` D ) )