This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmbr3v

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypothesis lmbr3v.1 
|- ( ph -> J e. ( TopOn ` X ) )
Assertion lmbr3v 
|- ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lmbr3v.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 eqid 
 |-  ( ZZ>= ` 0 ) = ( ZZ>= ` 0 )
3 0zd 
 |-  ( ph -> 0 e. ZZ )
4 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. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
5 0z 
 |-  0 e. ZZ
6 2 rexuz3 
 |-  ( 0 e. ZZ -> ( E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
7 5 6 ax-mp 
 |-  ( E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
8 7 imbi2i 
 |-  ( ( P e. u -> E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
9 8 ralbii 
 |-  ( A. u e. J ( P e. u -> E. j e. ( ZZ>= ` 0 ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
10 9 3anbi3i 
 |-  ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ( ZZ>= ` 0 ) 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. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
11 4 10 bitrdi 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )