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 ∞Met X F Cau D F X 𝑝𝑚 x + j k j k dom F F k X F k D F j < x

Proof

Step Hyp Ref Expression
1 iscau D ∞Met X F Cau D F X 𝑝𝑚 x + j F j : j F j ball D x
2 elfvdm D ∞Met X X dom ∞Met
3 cnex V
4 elpmg X dom ∞Met V F X 𝑝𝑚 Fun F F × X
5 2 3 4 sylancl D ∞Met X F X 𝑝𝑚 Fun F F × X
6 5 simprbda D ∞Met X F X 𝑝𝑚 Fun F
7 ffvresb Fun F F j : j F j ball D x k j k dom F F k F j ball D x
8 6 7 syl D ∞Met X F X 𝑝𝑚 F j : j F j ball D x k j k dom F F k F j ball D x
9 8 rexbidv D ∞Met X F X 𝑝𝑚 j F j : j F j ball D x j k j k dom F F k F j ball D x
10 9 adantr D ∞Met X F X 𝑝𝑚 x + j F j : j F j ball D x j k j k dom F F k F j ball D x
11 uzid j j j
12 11 adantl D ∞Met X x + j j j
13 eleq1w k = j k dom F j dom F
14 fveq2 k = j F k = F j
15 14 eleq1d k = j F k F j ball D x F j F j ball D x
16 13 15 anbi12d k = j k dom F F k F j ball D x j dom F F j F j ball D x
17 16 rspcv j j k j k dom F F k F j ball D x j dom F F j F j ball D x
18 12 17 syl D ∞Met X x + j k j k dom F F k F j ball D x j dom F F j F j ball D x
19 n0i F j F j ball D x ¬ F j ball D x =
20 blf D ∞Met X ball D : X × * 𝒫 X
21 20 fdmd D ∞Met X dom ball D = X × *
22 ndmovg dom ball D = X × * ¬ F j X x * F j ball D x =
23 22 ex dom ball D = X × * ¬ F j X x * F j ball D x =
24 21 23 syl D ∞Met X ¬ F j X x * F j ball D x =
25 24 con1d D ∞Met X ¬ F j ball D x = F j X x *
26 simpl F j X x * F j X
27 19 25 26 syl56 D ∞Met X F j F j ball D x F j X
28 27 adantld D ∞Met X j dom F F j F j ball D x F j X
29 28 ad2antrr D ∞Met X x + j j dom F F j F j ball D x F j X
30 18 29 syld D ∞Met X x + j k j k dom F F k F j ball D x F j X
31 14 eleq1d k = j F k X F j X
32 14 oveq1d k = j F k D F j = F j D F j
33 32 breq1d k = j F k D F j < x F j D F j < x
34 13 31 33 3anbi123d k = j k dom F F k X F k D F j < x j dom F F j X F j D F j < x
35 34 rspcv j j k j k dom F F k X F k D F j < x j dom F F j X F j D F j < x
36 12 35 syl D ∞Met X x + j k j k dom F F k X F k D F j < x j dom F F j X F j D F j < x
37 simp2 j dom F F j X F j D F j < x F j X
38 36 37 syl6 D ∞Met X x + j k j k dom F F k X F k D F j < x F j X
39 rpxr x + x *
40 elbl D ∞Met X F j X x * F k F j ball D x F k X F j D F k < x
41 39 40 syl3an3 D ∞Met X F j X x + F k F j ball D x F k X F j D F k < x
42 xmetsym D ∞Met X F j X F k X F j D F k = F k D F j
43 42 3expa D ∞Met X F j X F k X F j D F k = F k D F j
44 43 3adantl3 D ∞Met X F j X x + F k X F j D F k = F k D F j
45 44 breq1d D ∞Met X F j X x + F k X F j D F k < x F k D F j < x
46 45 pm5.32da D ∞Met X F j X x + F k X F j D F k < x F k X F k D F j < x
47 41 46 bitrd D ∞Met X F j X x + F k F j ball D x F k X F k D F j < x
48 47 3com23 D ∞Met X x + F j X F k F j ball D x F k X F k D F j < x
49 48 anbi2d D ∞Met X x + F j X k dom F F k F j ball D x k dom F F k X F k D F j < x
50 3anass k dom F F k X F k D F j < x k dom F F k X F k D F j < x
51 49 50 bitr4di D ∞Met X x + F j X k dom F F k F j ball D x k dom F F k X F k D F j < x
52 51 ralbidv D ∞Met X x + F j X k j k dom F F k F j ball D x k j k dom F F k X F k D F j < x
53 52 3expia D ∞Met X x + F j X k j k dom F F k F j ball D x k j k dom F F k X F k D F j < x
54 53 adantr D ∞Met X x + j F j X k j k dom F F k F j ball D x k j k dom F F k X F k D F j < x
55 30 38 54 pm5.21ndd D ∞Met X x + j k j k dom F F k F j ball D x k j k dom F F k X F k D F j < x
56 55 rexbidva D ∞Met X x + j k j k dom F F k F j ball D x j k j k dom F F k X F k D F j < x
57 56 adantlr D ∞Met X F X 𝑝𝑚 x + j k j k dom F F k F j ball D x j k j k dom F F k X F k D F j < x
58 10 57 bitrd D ∞Met X F X 𝑝𝑚 x + j F j : j F j ball D x j k j k dom F F k X F k D F j < x
59 58 ralbidva D ∞Met X F X 𝑝𝑚 x + j F j : j F j ball D x x + j k j k dom F F k X F k D F j < x
60 59 pm5.32da D ∞Met X F X 𝑝𝑚 x + j F j : j F j ball D x F X 𝑝𝑚 x + j k j k dom F F k X F k D F j < x
61 1 60 bitrd D ∞Met X F Cau D F X 𝑝𝑚 x + j k j k dom F F k X F k D F j < x