This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscauf

Description: Express the property " F is a Cauchy sequence of metric D " presupposing F is a function. (Contributed by NM, 24-Jul-2007) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses iscau3.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iscau3.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
iscau3.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iscau4.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
iscau4.6 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = 𝐵 )
iscauf.7 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
Assertion iscauf ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 iscau3.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iscau3.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 iscau3.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 iscau4.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5 iscau4.6 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = 𝐵 )
6 iscauf.7 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
7 elfvdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
8 2 7 syl ⊢ ( 𝜑 → 𝑋 ∈ dom ∞Met )
9 cnex ⊢ ℂ ∈ V
10 8 9 jctir ⊢ ( 𝜑 → ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) )
11 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
12 zsscn ⊢ ℤ ⊆ ℂ
13 11 12 sstri ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℂ
14 1 13 eqsstri ⊢ 𝑍 ⊆ ℂ
15 6 14 jctir ⊢ ( 𝜑 → ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑍 ⊆ ℂ ) )
16 elpm2r ⊢ ( ( ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑍 ⊆ ℂ ) ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
17 10 15 16 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
18 17 biantrurd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) ) )
19 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
20 5 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) = 𝐵 )
21 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐹 : 𝑍 ⟶ 𝑋 )
22 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ 𝑍 )
23 21 22 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 )
24 20 23 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐵 ∈ 𝑋 )
25 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
26 25 4 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
27 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
28 6 25 27 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
29 26 28 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐴 ∈ 𝑋 )
30 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
31 19 24 29 30 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
32 31 breq1d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) )
33 fdm ⊢ ( 𝐹 : 𝑍 ⟶ 𝑋 → dom 𝐹 = 𝑍 )
34 33 eleq2d ⊢ ( 𝐹 : 𝑍 ⟶ 𝑋 → ( 𝑘 ∈ dom 𝐹 ↔ 𝑘 ∈ 𝑍 ) )
35 34 biimpar ⊢ ( ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ dom 𝐹 )
36 6 25 35 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑘 ∈ dom 𝐹 )
37 36 29 jca ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ) )
38 37 biantrurd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐴 𝐷 𝐵 ) < 𝑥 ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
39 df-3an ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) )
40 38 39 bitr4di ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐴 𝐷 𝐵 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
41 32 40 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
42 41 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
43 42 ralbidva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
44 43 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
45 44 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
46 1 2 3 4 5 iscau4 ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) ) )
47 18 45 46 3bitr4rd ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ) )