Metamath Proof Explorer

Theorem lmbr3

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
Hypotheses lmbr3.1 
|- F/_ k F
lmbr3.2 
|- ( ph -> J e. ( TopOn ` X ) )
Assertion lmbr3 
|- ( 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 lmbr3.1 
 |-  F/_ k F
2 lmbr3.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 2 lmbr3v 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. v e. J ( P e. v -> E. i e. ZZ A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. v ) ) ) ) )
4 eleq2w 
 |-  ( v = u -> ( P e. v <-> P e. u ) )
5 eleq2w 
 |-  ( v = u -> ( ( F ` l ) e. v <-> ( F ` l ) e. u ) )
6 5 anbi2d 
 |-  ( v = u -> ( ( l e. dom F /\ ( F ` l ) e. v ) <-> ( l e. dom F /\ ( F ` l ) e. u ) ) )
7 6 rexralbidv 
 |-  ( v = u -> ( E. i e. ZZ A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. v ) <-> E. i e. ZZ A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. u ) ) )
8 fveq2 
 |-  ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) )
9 8 raleqdv 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. u ) <-> A. l e. ( ZZ>= ` j ) ( l e. dom F /\ ( F ` l ) e. u ) ) )
10 nfcv 
 |-  F/_ k l
11 1 nfdm 
 |-  F/_ k dom F
12 10 11 nfel 
 |-  F/ k l e. dom F
13 1 10 nffv 
 |-  F/_ k ( F ` l )
14 nfcv 
 |-  F/_ k u
15 13 14 nfel 
 |-  F/ k ( F ` l ) e. u
16 12 15 nfan 
 |-  F/ k ( l e. dom F /\ ( F ` l ) e. u )
17 nfv 
 |-  F/ l ( k e. dom F /\ ( F ` k ) e. u )
18 eleq1w 
 |-  ( l = k -> ( l e. dom F <-> k e. dom F ) )
19 fveq2 
 |-  ( l = k -> ( F ` l ) = ( F ` k ) )
20 19 eleq1d 
 |-  ( l = k -> ( ( F ` l ) e. u <-> ( F ` k ) e. u ) )
21 18 20 anbi12d 
 |-  ( l = k -> ( ( l e. dom F /\ ( F ` l ) e. u ) <-> ( k e. dom F /\ ( F ` k ) e. u ) ) )
22 16 17 21 cbvralw 
 |-  ( A. l e. ( ZZ>= ` j ) ( l e. dom F /\ ( F ` l ) e. u ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
23 9 22 bitrdi 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. u ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
24 23 cbvrexvw 
 |-  ( E. i e. ZZ A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
25 7 24 bitrdi 
 |-  ( v = u -> ( E. i e. ZZ A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. v ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
26 4 25 imbi12d 
 |-  ( v = u -> ( ( P e. v -> E. i e. ZZ A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. v ) ) <-> ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
27 26 cbvralvw 
 |-  ( A. v e. J ( P e. v -> E. i e. ZZ A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. v ) ) <-> A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
28 27 3anbi3i 
 |-  ( ( F e. ( X ^pm CC ) /\ P e. X /\ A. v e. J ( P e. v -> E. i e. ZZ A. l e. ( ZZ>= ` i ) ( l e. dom F /\ ( F ` l ) e. v ) ) ) <-> ( 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 ) ) ) )
29 3 28 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 ) ) ) ) )