Metamath Proof Explorer

Theorem lmbrf

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 lmbr2 presupposes that F is a function. (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypotheses lmbr.2 
|- ( ph -> J e. ( TopOn ` X ) )
lmbr2.4 
|- Z = ( ZZ>= ` M )
lmbr2.5 
|- ( ph -> M e. ZZ )
lmbrf.6 
|- ( ph -> F : Z --> X )
lmbrf.7 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
Assertion lmbrf 
|- ( ph -> ( F ( ~~>t ` J ) P <-> ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) ) ) )

Proof

Step Hyp Ref Expression
1 lmbr.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 lmbr2.4 
 |-  Z = ( ZZ>= ` M )
3 lmbr2.5 
 |-  ( ph -> M e. ZZ )
4 lmbrf.6 
 |-  ( ph -> F : Z --> X )
5 lmbrf.7 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
6 1 2 3 lmbr2 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
7 3anass 
 |-  ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) <-> ( F e. ( X ^pm CC ) /\ ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
8 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
9 5 eleq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) e. u <-> A e. u ) )
10 4 fdmd 
 |-  ( ph -> dom F = Z )
11 10 eleq2d 
 |-  ( ph -> ( k e. dom F <-> k e. Z ) )
12 11 biimpar 
 |-  ( ( ph /\ k e. Z ) -> k e. dom F )
13 12 biantrurd 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) e. u <-> ( k e. dom F /\ ( F ` k ) e. u ) ) )
14 9 13 bitr3d 
 |-  ( ( ph /\ k e. Z ) -> ( A e. u <-> ( k e. dom F /\ ( F ` k ) e. u ) ) )
15 8 14 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( A e. u <-> ( k e. dom F /\ ( F ` k ) e. u ) ) )
16 15 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( A e. u <-> ( k e. dom F /\ ( F ` k ) e. u ) ) )
17 16 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A e. u <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
18 17 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A e. u <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
19 18 imbi2d 
 |-  ( ph -> ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) <-> ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
20 19 ralbidv 
 |-  ( ph -> ( A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) <-> A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
21 20 anbi2d 
 |-  ( ph -> ( ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) ) <-> ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
22 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
23 1 22 syl 
 |-  ( ph -> X e. J )
24 cnex 
 |-  CC e. _V
25 23 24 jctir 
 |-  ( ph -> ( X e. J /\ CC e. _V ) )
26 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
27 zsscn 
 |-  ZZ C_ CC
28 26 27 sstri 
 |-  ( ZZ>= ` M ) C_ CC
29 2 28 eqsstri 
 |-  Z C_ CC
30 4 29 jctir 
 |-  ( ph -> ( F : Z --> X /\ Z C_ CC ) )
31 elpm2r 
 |-  ( ( ( X e. J /\ CC e. _V ) /\ ( F : Z --> X /\ Z C_ CC ) ) -> F e. ( X ^pm CC ) )
32 25 30 31 syl2anc 
 |-  ( ph -> F e. ( X ^pm CC ) )
33 32 biantrurd 
 |-  ( ph -> ( ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) <-> ( F e. ( X ^pm CC ) /\ ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) ) )
34 21 33 bitr2d 
 |-  ( ph -> ( ( F e. ( X ^pm CC ) /\ ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) <-> ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) ) ) )
35 7 34 bitrid 
 |-  ( ph -> ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) <-> ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) ) ) )
36 6 35 bitrd 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) ) ) )