Metamath Proof Explorer


Theorem lmmbrf

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 presupposes that F is a function. (Contributed by NM, 20-Jul-2007) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 J = MetOpen D
lmmbr.3 φ D ∞Met X
lmmbr3.5 Z = M
lmmbr3.6 φ M
lmmbrf.7 φ k Z F k = A
lmmbrf.8 φ F : Z X
Assertion lmmbrf φ F t J P P X x + j Z k j A D P < x

Proof

Step Hyp Ref Expression
1 lmmbr.2 J = MetOpen D
2 lmmbr.3 φ D ∞Met X
3 lmmbr3.5 Z = M
4 lmmbr3.6 φ M
5 lmmbrf.7 φ k Z F k = A
6 lmmbrf.8 φ F : Z X
7 elfvdm D ∞Met X X dom ∞Met
8 cnex V
9 7 8 jctir D ∞Met X X dom ∞Met V
10 uzssz M
11 zsscn
12 10 11 sstri M
13 3 12 eqsstri Z
14 13 jctr F : Z X F : Z X Z
15 elpm2r X dom ∞Met V F : Z X Z F X 𝑝𝑚
16 9 14 15 syl2an D ∞Met X F : Z X F X 𝑝𝑚
17 2 6 16 syl2anc φ F X 𝑝𝑚
18 17 biantrurd φ P X x + j Z k j k dom F F k X F k D P < x F X 𝑝𝑚 P X x + j Z k j k dom F F k X F k D P < x
19 3 uztrn2 j Z k j k Z
20 19 adantll φ j Z k j k Z
21 5 oveq1d φ k Z F k D P = A D P
22 21 breq1d φ k Z F k D P < x A D P < x
23 22 adantrl φ j Z k Z F k D P < x A D P < x
24 6 fdmd φ dom F = Z
25 24 eleq2d φ k dom F k Z
26 25 biimpar φ k Z k dom F
27 6 ffvelrnda φ k Z F k X
28 26 27 jca φ k Z k dom F F k X
29 28 biantrurd φ k Z F k D P < x k dom F F k X F k D P < x
30 df-3an k dom F F k X F k D P < x k dom F F k X F k D P < x
31 29 30 bitr4di φ k Z F k D P < x k dom F F k X F k D P < x
32 31 adantrl φ j Z k Z F k D P < x k dom F F k X F k D P < x
33 23 32 bitr3d φ j Z k Z A D P < x k dom F F k X F k D P < x
34 33 anassrs φ j Z k Z A D P < x k dom F F k X F k D P < x
35 20 34 syldan φ j Z k j A D P < x k dom F F k X F k D P < x
36 35 ralbidva φ j Z k j A D P < x k j k dom F F k X F k D P < x
37 36 rexbidva φ j Z k j A D P < x j Z k j k dom F F k X F k D P < x
38 37 ralbidv φ x + j Z k j A D P < x x + j Z k j k dom F F k X F k D P < x
39 38 anbi2d φ P X x + j Z k j A D P < x P X x + j Z k j k dom F F k X F k D P < x
40 1 2 3 4 lmmbr3 φ F t J P F X 𝑝𝑚 P X x + j Z k j k dom F F k X F k D P < x
41 3anass F X 𝑝𝑚 P X x + j Z k j k dom F F k X F k D P < x F X 𝑝𝑚 P X x + j Z k j k dom F F k X F k D P < x
42 40 41 bitrdi φ F t J P F X 𝑝𝑚 P X x + j Z k j k dom F F k X F k D P < x
43 18 39 42 3bitr4rd φ F t J P P X x + j Z k j A D P < x