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 ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )