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 ‘ 𝐷 ) ) )