Metamath Proof Explorer

Theorem caures

Description: The restriction of a Cauchy sequence to an upper set of integers is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses caures.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
caures.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
caures.4 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
caures.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
Assertion caures ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ↾ 𝑍 ) ∈ ( Cau ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 caures.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 caures.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 caures.4 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
4 caures.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
5 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
6 5 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
7 6 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 ∈ dom 𝐹 ↔ ( 𝑘 ∈ 𝑍 ∧ 𝑘 ∈ dom 𝐹 ) ) )
8 dmres ⊢ dom ( 𝐹 ↾ 𝑍 ) = ( 𝑍 ∩ dom 𝐹 )
9 8 elin2 ⊢ ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ↔ ( 𝑘 ∈ 𝑍 ∧ 𝑘 ∈ dom 𝐹 ) )
10 7 9 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 ∈ dom 𝐹 ↔ 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ) )
11 10 3anbi1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
12 11 ralbidva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
13 12 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
14 13 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
15 4 biantrurd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
16 elfvdm ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝑋 ∈ dom Met )
17 3 16 syl ⊢ ( 𝜑 → 𝑋 ∈ dom Met )
18 cnex ⊢ ℂ ∈ V
19 ssid ⊢ 𝑋 ⊆ 𝑋
20 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
21 zsscn ⊢ ℤ ⊆ ℂ
22 20 21 sstri ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℂ
23 1 22 eqsstri ⊢ 𝑍 ⊆ ℂ
24 pmss12g ⊢ ( ( ( 𝑋 ⊆ 𝑋 ∧ 𝑍 ⊆ ℂ ) ∧ ( 𝑋 ∈ dom Met ∧ ℂ ∈ V ) ) → ( 𝑋 ↑pm 𝑍 ) ⊆ ( 𝑋 ↑pm ℂ ) )
25 19 23 24 mpanl12 ⊢ ( ( 𝑋 ∈ dom Met ∧ ℂ ∈ V ) → ( 𝑋 ↑pm 𝑍 ) ⊆ ( 𝑋 ↑pm ℂ ) )
26 17 18 25 sylancl ⊢ ( 𝜑 → ( 𝑋 ↑pm 𝑍 ) ⊆ ( 𝑋 ↑pm ℂ ) )
27 1 fvexi ⊢ 𝑍 ∈ V
28 pmresg ⊢ ( ( 𝑍 ∈ V ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm 𝑍 ) )
29 27 4 28 sylancr ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm 𝑍 ) )
30 26 29 sseldd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm ℂ ) )
31 30 biantrurd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
32 14 15 31 3bitr3d ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ↔ ( ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
33 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
34 3 33 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
35 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
36 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
37 1 34 2 35 36 iscau4 ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
38 fvres ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐹 ↾ 𝑍 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ↾ 𝑍 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
40 fvres ⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝐹 ↾ 𝑍 ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝐹 ↾ 𝑍 ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
42 1 34 2 39 41 iscau4 ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑍 ) ∈ ( Cau ‘ 𝐷 ) ↔ ( ( 𝐹 ↾ 𝑍 ) ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
43 32 37 42 3bitr4d ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ↾ 𝑍 ) ∈ ( Cau ‘ 𝐷 ) ) )