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 
|- ( ph -> D e. ( *Met ` X ) )
lmmbr3.5 
|- Z = ( ZZ>= ` M )
lmmbr3.6 
|- ( ph -> M e. ZZ )
lmmbrf.7 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
lmmbrf.8 
|- ( ph -> F : Z --> X )
Assertion lmmbrf 
|- ( ph -> ( F ( ~~>t ` J ) P <-> ( P e. X /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( A D P ) < x ) ) )

Proof

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