# 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 ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\in \mathrm{Cau}\left({D}\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 iscau ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\in \mathrm{Cau}\left({D}\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)$
2 elfvdm ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}\in \mathrm{dom}\mathrm{\infty Met}$
3 cnex ${⊢}ℂ\in \mathrm{V}$
4 elpmg ${⊢}\left({X}\in \mathrm{dom}\mathrm{\infty Met}\wedge ℂ\in \mathrm{V}\right)\to \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)↔\left(\mathrm{Fun}{F}\wedge {F}\subseteq ℂ×{X}\right)\right)$
5 2 3 4 sylancl ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)↔\left(\mathrm{Fun}{F}\wedge {F}\subseteq ℂ×{X}\right)\right)$
6 5 simprbda ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)\to \mathrm{Fun}{F}$
7 ffvresb ${⊢}\mathrm{Fun}{F}\to \left(\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
8 6 7 syl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)\to \left(\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
9 8 rexbidv ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)\to \left(\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
10 9 adantr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
11 uzid ${⊢}{j}\in ℤ\to {j}\in {ℤ}_{\ge {j}}$
12 11 adantl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\to {j}\in {ℤ}_{\ge {j}}$
13 eleq1w ${⊢}{k}={j}\to \left({k}\in \mathrm{dom}{F}↔{j}\in \mathrm{dom}{F}\right)$
14 fveq2 ${⊢}{k}={j}\to {F}\left({k}\right)={F}\left({j}\right)$
15 14 eleq1d ${⊢}{k}={j}\to \left({F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)↔{F}\left({j}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)$
16 13 15 anbi12d ${⊢}{k}={j}\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
17 16 rspcv ${⊢}{j}\in {ℤ}_{\ge {j}}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\to \left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
18 12 17 syl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\to \left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
19 n0i ${⊢}{F}\left({j}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\to ¬{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}=\varnothing$
20 blf ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{ball}\left({D}\right):{X}×{ℝ}^{*}⟶𝒫{X}$
21 20 fdmd ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{dom}\mathrm{ball}\left({D}\right)={X}×{ℝ}^{*}$
22 ndmovg ${⊢}\left(\mathrm{dom}\mathrm{ball}\left({D}\right)={X}×{ℝ}^{*}\wedge ¬\left({F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{*}\right)\right)\to {F}\left({j}\right)\mathrm{ball}\left({D}\right){x}=\varnothing$
23 22 ex ${⊢}\mathrm{dom}\mathrm{ball}\left({D}\right)={X}×{ℝ}^{*}\to \left(¬\left({F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{*}\right)\to {F}\left({j}\right)\mathrm{ball}\left({D}\right){x}=\varnothing \right)$
24 21 23 syl ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(¬\left({F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{*}\right)\to {F}\left({j}\right)\mathrm{ball}\left({D}\right){x}=\varnothing \right)$
25 24 con1d ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(¬{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}=\varnothing \to \left({F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{*}\right)\right)$
26 simpl ${⊢}\left({F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{*}\right)\to {F}\left({j}\right)\in {X}$
27 19 25 26 syl56 ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\left({j}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\to {F}\left({j}\right)\in {X}\right)$
28 27 adantld ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(\left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\to {F}\left({j}\right)\in {X}\right)$
29 28 ad2antrr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\to \left(\left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\to {F}\left({j}\right)\in {X}\right)$
30 18 29 syld ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)\to {F}\left({j}\right)\in {X}\right)$
31 14 eleq1d ${⊢}{k}={j}\to \left({F}\left({k}\right)\in {X}↔{F}\left({j}\right)\in {X}\right)$
32 14 oveq1d ${⊢}{k}={j}\to {F}\left({k}\right){D}{F}\left({j}\right)={F}\left({j}\right){D}{F}\left({j}\right)$
33 32 breq1d ${⊢}{k}={j}\to \left({F}\left({k}\right){D}{F}\left({j}\right)<{x}↔{F}\left({j}\right){D}{F}\left({j}\right)<{x}\right)$
34 13 31 33 3anbi123d ${⊢}{k}={j}\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)↔\left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in {X}\wedge {F}\left({j}\right){D}{F}\left({j}\right)<{x}\right)\right)$
35 34 rspcv ${⊢}{j}\in {ℤ}_{\ge {j}}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to \left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in {X}\wedge {F}\left({j}\right){D}{F}\left({j}\right)<{x}\right)\right)$
36 12 35 syl ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to \left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in {X}\wedge {F}\left({j}\right){D}{F}\left({j}\right)<{x}\right)\right)$
37 simp2 ${⊢}\left({j}\in \mathrm{dom}{F}\wedge {F}\left({j}\right)\in {X}\wedge {F}\left({j}\right){D}{F}\left({j}\right)<{x}\right)\to {F}\left({j}\right)\in {X}$
38 36 37 syl6 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to {F}\left({j}\right)\in {X}\right)$
39 rpxr ${⊢}{x}\in {ℝ}^{+}\to {x}\in {ℝ}^{*}$
40 elbl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{*}\right)\to \left({F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({j}\right){D}{F}\left({k}\right)<{x}\right)\right)$
41 39 40 syl3an3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{+}\right)\to \left({F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({j}\right){D}{F}\left({k}\right)<{x}\right)\right)$
42 xmetsym ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({j}\right)\in {X}\wedge {F}\left({k}\right)\in {X}\right)\to {F}\left({j}\right){D}{F}\left({k}\right)={F}\left({k}\right){D}{F}\left({j}\right)$
43 42 3expa ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({j}\right)\in {X}\right)\wedge {F}\left({k}\right)\in {X}\right)\to {F}\left({j}\right){D}{F}\left({k}\right)={F}\left({k}\right){D}{F}\left({j}\right)$
44 43 3adantl3 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{+}\right)\wedge {F}\left({k}\right)\in {X}\right)\to {F}\left({j}\right){D}{F}\left({k}\right)={F}\left({k}\right){D}{F}\left({j}\right)$
45 44 breq1d ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{+}\right)\wedge {F}\left({k}\right)\in {X}\right)\to \left({F}\left({j}\right){D}{F}\left({k}\right)<{x}↔{F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)$
46 45 pm5.32da ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{+}\right)\to \left(\left({F}\left({k}\right)\in {X}\wedge {F}\left({j}\right){D}{F}\left({k}\right)<{x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
47 41 46 bitrd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\left({j}\right)\in {X}\wedge {x}\in {ℝ}^{+}\right)\to \left({F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
48 47 3com23 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\wedge {F}\left({j}\right)\in {X}\right)\to \left({F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
49 48 anbi2d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\wedge {F}\left({j}\right)\in {X}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\left({k}\in \mathrm{dom}{F}\wedge \left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\right)$
50 3anass ${⊢}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)↔\left({k}\in \mathrm{dom}{F}\wedge \left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
51 49 50 syl6bbr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\wedge {F}\left({j}\right)\in {X}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
52 51 ralbidv ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\wedge {F}\left({j}\right)\in {X}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
53 52 3expia ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left({F}\left({j}\right)\in {X}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\right)$
54 53 adantr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\to \left({F}\left({j}\right)\in {X}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\right)$
55 30 38 54 pm5.21ndd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
56 55 rexbidva ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
57 56 adantlr ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)\right)↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
58 10 57 bitrd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
59 58 ralbidva ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
60 59 pm5.32da ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{F}\left({j}\right)\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\right)$
61 1 60 bitrd ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\in \mathrm{Cau}\left({D}\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\right)$