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 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 caufpm ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝐹 ∈ ( 𝑋pm ℂ ) )
2 elfvdm ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
3 cnex ℂ ∈ V
4 elpmg ( ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) → ( 𝐹 ∈ ( 𝑋pm ℂ ) ↔ ( Fun 𝐹𝐹 ⊆ ( ℂ × 𝑋 ) ) ) )
5 2 3 4 sylancl ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( 𝑋pm ℂ ) ↔ ( Fun 𝐹𝐹 ⊆ ( ℂ × 𝑋 ) ) ) )
6 5 biimpa ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋pm ℂ ) ) → ( Fun 𝐹𝐹 ⊆ ( ℂ × 𝑋 ) ) )
7 1 6 syldan ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ( Fun 𝐹𝐹 ⊆ ( ℂ × 𝑋 ) ) )
8 rnss ( 𝐹 ⊆ ( ℂ × 𝑋 ) → ran 𝐹 ⊆ ran ( ℂ × 𝑋 ) )
9 7 8 simpl2im ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹 ⊆ ran ( ℂ × 𝑋 ) )
10 rnxpss ran ( ℂ × 𝑋 ) ⊆ 𝑋
11 9 10 sstrdi ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹𝑋 )
12 11 adantlr ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹𝑋 )
13 frn ( 𝐹 : ℕ ⟶ 𝑌 → ran 𝐹𝑌 )
14 13 ad2antlr ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹𝑌 )
15 12 14 ssind ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ran 𝐹 ⊆ ( 𝑋𝑌 ) )
16 15 ex ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) → ran 𝐹 ⊆ ( 𝑋𝑌 ) ) )
17 xmetres ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋𝑌 ) ) )
18 caufpm ( ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋𝑌 ) ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝐹 ∈ ( ( 𝑋𝑌 ) ↑pm ℂ ) )
19 17 18 sylan ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝐹 ∈ ( ( 𝑋𝑌 ) ↑pm ℂ ) )
20 inex1g ( 𝑋 ∈ dom ∞Met → ( 𝑋𝑌 ) ∈ V )
21 2 20 syl ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋𝑌 ) ∈ V )
22 elpmg ( ( ( 𝑋𝑌 ) ∈ V ∧ ℂ ∈ V ) → ( 𝐹 ∈ ( ( 𝑋𝑌 ) ↑pm ℂ ) ↔ ( Fun 𝐹𝐹 ⊆ ( ℂ × ( 𝑋𝑌 ) ) ) ) )
23 21 3 22 sylancl ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( ( 𝑋𝑌 ) ↑pm ℂ ) ↔ ( Fun 𝐹𝐹 ⊆ ( ℂ × ( 𝑋𝑌 ) ) ) ) )
24 23 biimpa ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝑋𝑌 ) ↑pm ℂ ) ) → ( Fun 𝐹𝐹 ⊆ ( ℂ × ( 𝑋𝑌 ) ) ) )
25 19 24 syldan ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( Fun 𝐹𝐹 ⊆ ( ℂ × ( 𝑋𝑌 ) ) ) )
26 rnss ( 𝐹 ⊆ ( ℂ × ( 𝑋𝑌 ) ) → ran 𝐹 ⊆ ran ( ℂ × ( 𝑋𝑌 ) ) )
27 25 26 simpl2im ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ran 𝐹 ⊆ ran ( ℂ × ( 𝑋𝑌 ) ) )
28 rnxpss ran ( ℂ × ( 𝑋𝑌 ) ) ⊆ ( 𝑋𝑌 )
29 27 28 sstrdi ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ran 𝐹 ⊆ ( 𝑋𝑌 ) )
30 29 ex ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) → ran 𝐹 ⊆ ( 𝑋𝑌 ) ) )
31 30 adantr ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) → ran 𝐹 ⊆ ( 𝑋𝑌 ) ) )
32 ffn ( 𝐹 : ℕ ⟶ 𝑌𝐹 Fn ℕ )
33 df-f ( 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ↔ ( 𝐹 Fn ℕ ∧ ran 𝐹 ⊆ ( 𝑋𝑌 ) ) )
34 33 simplbi2 ( 𝐹 Fn ℕ → ( ran 𝐹 ⊆ ( 𝑋𝑌 ) → 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) )
35 32 34 syl ( 𝐹 : ℕ ⟶ 𝑌 → ( ran 𝐹 ⊆ ( 𝑋𝑌 ) → 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) )
36 inss2 ( 𝑋𝑌 ) ⊆ 𝑌
37 36 a1i ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋𝑌 ) ⊆ 𝑌 )
38 fss ( ( 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ∧ ( 𝑋𝑌 ) ⊆ 𝑌 ) → 𝐹 : ℕ ⟶ 𝑌 )
39 37 38 sylan2 ( ( 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → 𝐹 : ℕ ⟶ 𝑌 )
40 39 ancoms ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → 𝐹 : ℕ ⟶ 𝑌 )
41 ffvelrn ( ( 𝐹 : ℕ ⟶ 𝑌𝑦 ∈ ℕ ) → ( 𝐹𝑦 ) ∈ 𝑌 )
42 41 adantr ( ( ( 𝐹 : ℕ ⟶ 𝑌𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( ℤ𝑦 ) ) → ( 𝐹𝑦 ) ∈ 𝑌 )
43 eluznn ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ( ℤ𝑦 ) ) → 𝑧 ∈ ℕ )
44 ffvelrn ( ( 𝐹 : ℕ ⟶ 𝑌𝑧 ∈ ℕ ) → ( 𝐹𝑧 ) ∈ 𝑌 )
45 43 44 sylan2 ( ( 𝐹 : ℕ ⟶ 𝑌 ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ( ℤ𝑦 ) ) ) → ( 𝐹𝑧 ) ∈ 𝑌 )
46 45 anassrs ( ( ( 𝐹 : ℕ ⟶ 𝑌𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( ℤ𝑦 ) ) → ( 𝐹𝑧 ) ∈ 𝑌 )
47 42 46 ovresd ( ( ( 𝐹 : ℕ ⟶ 𝑌𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( ℤ𝑦 ) ) → ( ( 𝐹𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑦 ) 𝐷 ( 𝐹𝑧 ) ) )
48 47 breq1d ( ( ( 𝐹 : ℕ ⟶ 𝑌𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( ℤ𝑦 ) ) → ( ( ( 𝐹𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹𝑧 ) ) < 𝑥 ↔ ( ( 𝐹𝑦 ) 𝐷 ( 𝐹𝑧 ) ) < 𝑥 ) )
49 48 ralbidva ( ( 𝐹 : ℕ ⟶ 𝑌𝑦 ∈ ℕ ) → ( ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹𝑧 ) ) < 𝑥 ↔ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) 𝐷 ( 𝐹𝑧 ) ) < 𝑥 ) )
50 49 rexbidva ( 𝐹 : ℕ ⟶ 𝑌 → ( ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹𝑧 ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) 𝐷 ( 𝐹𝑧 ) ) < 𝑥 ) )
51 50 ralbidv ( 𝐹 : ℕ ⟶ 𝑌 → ( ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹𝑧 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) 𝐷 ( 𝐹𝑧 ) ) < 𝑥 ) )
52 40 51 syl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → ( ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹𝑧 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) 𝐷 ( 𝐹𝑧 ) ) < 𝑥 ) )
53 nnuz ℕ = ( ℤ ‘ 1 )
54 17 adantr ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋𝑌 ) ) )
55 1zzd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → 1 ∈ ℤ )
56 eqidd ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) ∧ 𝑧 ∈ ℕ ) → ( 𝐹𝑧 ) = ( 𝐹𝑧 ) )
57 eqidd ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝐹𝑦 ) = ( 𝐹𝑦 ) )
58 simpr ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) )
59 53 54 55 56 57 58 iscauf ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → ( 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ( 𝐹𝑧 ) ) < 𝑥 ) )
60 simpl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
61 id ( 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) → 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) )
62 inss1 ( 𝑋𝑌 ) ⊆ 𝑋
63 62 a1i ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋𝑌 ) ⊆ 𝑋 )
64 fss ( ( 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ∧ ( 𝑋𝑌 ) ⊆ 𝑋 ) → 𝐹 : ℕ ⟶ 𝑋 )
65 61 63 64 syl2anr ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → 𝐹 : ℕ ⟶ 𝑋 )
66 53 60 55 56 57 65 iscauf ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( ( 𝐹𝑦 ) 𝐷 ( 𝐹𝑧 ) ) < 𝑥 ) )
67 52 59 66 3bitr4rd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
68 67 ex ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 : ℕ ⟶ ( 𝑋𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ) )
69 35 68 sylan9r ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( ran 𝐹 ⊆ ( 𝑋𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ) )
70 16 31 69 pm5.21ndd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : ℕ ⟶ 𝑌 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐹 ∈ ( Cau ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )