Metamath Proof Explorer

Theorem lmcau

Description: Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of Kreyszig p. 28. (Contributed by NM, 29-Jan-2008) (Proof shortened by Mario Carneiro, 5-May-2014)

Ref Expression
Hypothesis lmcau.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion lmcau ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom ( ⇝𝑡 ‘ 𝐽 ) ⊆ ( Cau ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 lmcau.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 methaus ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )
3 lmfun ⊢ ( 𝐽 ∈ Haus → Fun ( ⇝𝑡 ‘ 𝐽 ) )
4 funfvbrb ⊢ ( Fun ( ⇝𝑡 ‘ 𝐽 ) → ( 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ↔ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) )
5 2 3 4 3syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ↔ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) )
6 id ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7 1 6 lmmbr ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ↔ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ∈ 𝑋 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
8 7 biimpa ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) → ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ∈ 𝑋 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
9 8 simp1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) → 𝑓 ∈ ( 𝑋 ↑pm ℂ ) )
10 simprr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
11 simplll ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
12 8 simp2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ∈ 𝑋 )
13 12 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ∈ 𝑋 )
14 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
15 14 ad2antlr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → 𝑥 ∈ ℝ )
16 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
17 16 ad2antrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
18 17 fvresd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) ‘ 𝑗 ) = ( 𝑓 ‘ 𝑗 ) )
19 10 17 ffvelrnd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) ‘ 𝑗 ) ∈ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
20 18 19 eqeltrrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( 𝑓 ‘ 𝑗 ) ∈ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
21 blhalf ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑓 ‘ 𝑗 ) ∈ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ⊆ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) )
22 11 13 15 20 21 syl22anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ⊆ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) )
23 10 22 fssd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℤ ∧ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) )
24 rphalfcl ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
25 8 simp3d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) 𝑦 ) )
26 oveq2 ⊢ ( 𝑦 = ( 𝑥 / 2 ) → ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) 𝑦 ) = ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
27 26 feq3d ⊢ ( 𝑦 = ( 𝑥 / 2 ) → ( ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) )
28 27 rexbidv ⊢ ( 𝑦 = ( 𝑥 / 2 ) → ( ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) )
29 28 rspcv ⊢ ( ( 𝑥 / 2 ) ∈ ℝ+ → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) )
30 24 25 29 syl2im ⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) → ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) )
31 30 impcom ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
32 uzf ⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
33 ffn ⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → ℤ≥ Fn ℤ )
34 reseq2 ⊢ ( 𝑢 = ( ℤ≥ ‘ 𝑗 ) → ( 𝑓 ↾ 𝑢 ) = ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) )
35 id ⊢ ( 𝑢 = ( ℤ≥ ‘ 𝑗 ) → 𝑢 = ( ℤ≥ ‘ 𝑗 ) )
36 34 35 feq12d ⊢ ( 𝑢 = ( ℤ≥ ‘ 𝑗 ) → ( ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ↔ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) )
37 36 rexrn ⊢ ( ℤ≥ Fn ℤ → ( ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ↔ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) )
38 32 33 37 mp2b ⊢ ( ∃ 𝑢 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑢 ) : 𝑢 ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ↔ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
39 31 38 sylib ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
40 23 39 reximddv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) )
41 40 ralrimiva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) )
42 iscau ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
43 42 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) → ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
44 9 41 43 mpbir2and ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) → 𝑓 ∈ ( Cau ‘ 𝐷 ) )
45 44 ex ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) → 𝑓 ∈ ( Cau ‘ 𝐷 ) ) )
46 5 45 sylbid ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) → 𝑓 ∈ ( Cau ‘ 𝐷 ) ) )
47 46 ssrdv ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom ( ⇝𝑡 ‘ 𝐽 ) ⊆ ( Cau ‘ 𝐷 ) )