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	ffvelcdmd	⊢ ( ( ( ( 𝐷 ∈ ( ∞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 ‘ 𝐷 ) )