Metamath Proof Explorer

Theorem iscau2

Description: Express the property " F is a Cauchy sequence of metric D " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion iscau2 ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 iscau ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
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 simprbda ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → Fun 𝐹 )
7 ffvresb ⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
8 6 7 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
9 8 rexbidv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
10 9 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
11 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
12 11 adantl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℤ ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
13 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ dom 𝐹 ↔ 𝑗 ∈ dom 𝐹 ) )
14 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
15 14 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) )
16 13 15 anbi12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
17 16 rspcv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) → ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
18 12 17 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) → ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
19 n0i ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) → ¬ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) = ∅ )
20 blf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )
21 20 fdmd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom ( ball ‘ 𝐷 ) = ( 𝑋 × ℝ* ) )
22 ndmovg ⊢ ( ( dom ( ball ‘ 𝐷 ) = ( 𝑋 × ℝ* ) ∧ ¬ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ* ) ) → ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) = ∅ )
23 22 ex ⊢ ( dom ( ball ‘ 𝐷 ) = ( 𝑋 × ℝ* ) → ( ¬ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) = ∅ ) )
24 21 23 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ¬ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) = ∅ ) )
25 24 con1d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ¬ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) = ∅ → ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ* ) ) )
26 simpl ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ* ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 )
27 19 25 26 syl56 ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) )
28 27 adantld ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) )
29 28 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℤ ) → ( ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) )
30 18 29 syld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) )
31 14 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ↔ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) )
32 14 oveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) )
33 32 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) )
34 13 31 33 3anbi123d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
35 34 rspcv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) → ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
36 12 35 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) → ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
37 simp2 ⊢ ( ( 𝑗 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 )
38 36 37 syl6 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) )
39 rpxr ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ* )
40 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) )
41 39 40 syl3an3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) )
42 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) )
43 42 3expa ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) )
44 43 3adantl3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) )
45 44 breq1d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) )
46 45 pm5.32da ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
47 41 46 bitrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
48 47 3com23 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
49 48 anbi2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
50 3anass ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
51 49 50 bitr4di ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
52 51 ralbidv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
53 52 3expia ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
54 53 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
55 30 38 54 pm5.21ndd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
56 55 rexbidva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
57 56 adantlr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
58 10 57 bitrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
59 58 ralbidva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) )
60 59 pm5.32da ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝐹 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )
61 1 60 bitrd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑥 ) ) ) )