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

Metamath Proof Explorer

Theorem iscmet3lem1

Description: Lemma for iscmet3 . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses iscmet3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iscmet3.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
iscmet3.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iscmet3.4 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
iscmet3.6 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
iscmet3.9 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℤ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
iscmet3.10 ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) )
Assertion iscmet3lem1 ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 iscmet3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iscmet3.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 iscmet3.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 iscmet3.4 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
5 iscmet3.6 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
6 iscmet3.9 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℤ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
7 iscmet3.10 ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) )
8 1 iscmet3lem3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 )
9 3 8 sylan ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 )
10 1 r19.2uz ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 → ∃ 𝑘 ∈ 𝑍 ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 )
11 9 10 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑘 ∈ 𝑍 ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 )
12 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑘 ) )
13 12 eleq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) ) )
14 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ 𝑍 ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) )
15 simpl ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑘 ∈ 𝑍 )
16 15 adantl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝑘 ∈ 𝑍 )
17 rsp ⊢ ( ∀ 𝑘 ∈ 𝑍 ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) → ( 𝑘 ∈ 𝑍 → ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) ) )
18 14 16 17 sylc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) )
19 16 1 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
20 eluzfz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ( 𝑀 ... 𝑘 ) )
21 19 20 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑘 ) )
22 13 18 21 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
23 12 eleq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑗 ) ∈ ( 𝑆 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑗 ) ∈ ( 𝑆 ‘ 𝑘 ) ) )
24 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑗 ) )
25 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
26 25 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑗 ) ∈ ( 𝑆 ‘ 𝑛 ) ) )
27 24 26 raleqbidv ⊢ ( 𝑘 = 𝑗 → ( ∀ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝐹 ‘ 𝑗 ) ∈ ( 𝑆 ‘ 𝑛 ) ) )
28 1 uztrn2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
29 28 adantl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝑗 ∈ 𝑍 )
30 27 14 29 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ∀ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝐹 ‘ 𝑗 ) ∈ ( 𝑆 ‘ 𝑛 ) )
31 simprr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) )
32 elfzuzb ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) )
33 19 31 32 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑗 ) )
34 23 30 33 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ( 𝑆 ‘ 𝑘 ) )
35 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ℤ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
36 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
37 36 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
38 37 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝑘 ∈ ℤ )
39 rsp ⊢ ( ∀ 𝑘 ∈ ℤ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) → ( 𝑘 ∈ ℤ → ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) )
40 35 38 39 sylc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
41 oveq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑘 ) → ( 𝑢 𝐷 𝑣 ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑣 ) )
42 41 breq1d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑘 ) → ( ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) )
43 oveq2 ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑗 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑣 ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) )
44 43 breq1d ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑗 ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) )
45 42 44 rspc2va ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ ( 𝑆 ‘ 𝑘 ) ) ∧ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑘 ) ∀ 𝑣 ∈ ( 𝑆 ‘ 𝑘 ) ( 𝑢 𝐷 𝑣 ) < ( ( 1 / 2 ) ↑ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
46 22 34 40 45 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( ( 1 / 2 ) ↑ 𝑘 ) )
47 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
48 5 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ 𝑋 )
49 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
50 48 15 49 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
51 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 )
52 48 28 51 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 )
53 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
54 47 50 52 53 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ )
55 1rp ⊢ 1 ∈ ℝ+
56 rphalfcl ⊢ ( 1 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ+ )
57 55 56 ax-mp ⊢ ( 1 / 2 ) ∈ ℝ+
58 rpexpcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ )
59 57 38 58 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ+ )
60 59 rpred ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ )
61 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
62 61 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → 𝑟 ∈ ℝ )
63 lttr ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) ∈ ℝ ∧ ( ( 1 / 2 ) ↑ 𝑘 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( ( 1 / 2 ) ↑ 𝑘 ) ∧ ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 ) )
64 54 60 62 63 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < ( ( 1 / 2 ) ↑ 𝑘 ) ∧ ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 ) )
65 46 64 mpand ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 ) )
66 65 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 ) )
67 66 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 ) )
68 67 reximdva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ 𝑍 ( ( 1 / 2 ) ↑ 𝑘 ) < 𝑟 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 ) )
69 11 68 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 )
70 69 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 )
71 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
72 4 71 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
73 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
74 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
75 1 72 3 73 74 5 iscauf ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑗 ) ) < 𝑟 ) )
76 70 75 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )