Metamath Proof Explorer

Theorem xlimbr

Description: Express the binary relation "sequence F converges to point P " w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses xlimbr.k 
|- F/_ k F
xlimbr.m 
|- ( ph -> M e. ZZ )
xlimbr.z 
|- Z = ( ZZ>= ` M )
xlimbr.f 
|- ( ph -> F : Z --> RR* )
xlimbr.j 
|- J = ( ordTop ` <_ )
Assertion xlimbr 
|- ( ph -> ( F ~~>* P <-> ( P e. RR* /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )

Proof

Step Hyp Ref Expression
1 xlimbr.k 
 |-  F/_ k F
2 xlimbr.m 
 |-  ( ph -> M e. ZZ )
3 xlimbr.z 
 |-  Z = ( ZZ>= ` M )
4 xlimbr.f 
 |-  ( ph -> F : Z --> RR* )
5 xlimbr.j 
 |-  J = ( ordTop ` <_ )
6 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
7 6 breqi 
 |-  ( F ~~>* P <-> F ( ~~>t ` ( ordTop ` <_ ) ) P )
8 7 a1i 
 |-  ( ph -> ( F ~~>* P <-> F ( ~~>t ` ( ordTop ` <_ ) ) P ) )
9 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
10 9 a1i 
 |-  ( ph -> ( ordTop ` <_ ) e. ( TopOn ` RR* ) )
11 1 10 lmbr3 
 |-  ( ph -> ( F ( ~~>t ` ( ordTop ` <_ ) ) P <-> ( F e. ( RR* ^pm CC ) /\ P e. RR* /\ A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
12 simpr2 
 |-  ( ( ph /\ ( F e. ( RR* ^pm CC ) /\ P e. RR* /\ A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) -> P e. RR* )
13 5 eqcomi 
 |-  ( ordTop ` <_ ) = J
14 13 raleqi 
 |-  ( A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ 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 ) ) )
15 3 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z 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 ) ) )
16 15 bicomd 
 |-  ( M e. ZZ -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
17 16 imbi2d 
 |-  ( M e. ZZ -> ( ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
18 17 biimpd 
 |-  ( M e. ZZ -> ( ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) -> ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
19 18 ralimdv 
 |-  ( M e. ZZ -> ( A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) 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 ) ) ) )
20 2 19 syl 
 |-  ( ph -> ( A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) 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 imp 
 |-  ( ( ph /\ A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) 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 ) ) )
22 14 21 sylan2b 
 |-  ( ( ph /\ A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) 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 ) ) )
23 22 3ad2antr3 
 |-  ( ( ph /\ ( F e. ( RR* ^pm CC ) /\ P e. RR* /\ A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) 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 ) ) )
24 12 23 jca 
 |-  ( ( ph /\ ( F e. ( RR* ^pm CC ) /\ P e. RR* /\ A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) -> ( P e. RR* /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
25 cnex 
 |-  CC e. _V
26 25 a1i 
 |-  ( ph -> CC e. _V )
27 10 elfvexd 
 |-  ( ph -> RR* e. _V )
28 3 uzsscn2 
 |-  Z C_ CC
29 28 a1i 
 |-  ( ph -> Z C_ CC )
30 26 27 29 4 fpmd 
 |-  ( ph -> F e. ( RR* ^pm CC ) )
31 30 adantr 
 |-  ( ( ph /\ ( P e. RR* /\ 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. ( RR* ^pm CC ) )
32 simprl 
 |-  ( ( ph /\ ( P e. RR* /\ 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. RR* )
33 17 biimprd 
 |-  ( M e. ZZ -> ( ( P e. u -> E. j e. Z 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 ) ) ) )
34 33 ralimdv 
 |-  ( M e. ZZ -> ( A. u e. J ( P e. u -> E. j e. Z 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 ) ) ) )
35 2 34 syl 
 |-  ( ph -> ( A. u e. J ( P e. u -> E. j e. Z 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 ) ) ) )
36 35 imp 
 |-  ( ( ph /\ A. u e. J ( P e. u -> E. j e. Z 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 ) ) )
37 5 raleqi 
 |-  ( A. u e. J ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
38 36 37 sylib 
 |-  ( ( ph /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) -> A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
39 38 adantrl 
 |-  ( ( ph /\ ( P e. RR* /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) -> A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
40 31 32 39 3jca 
 |-  ( ( ph /\ ( P e. RR* /\ 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. ( RR* ^pm CC ) /\ P e. RR* /\ A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
41 24 40 impbida 
 |-  ( ph -> ( ( F e. ( RR* ^pm CC ) /\ P e. RR* /\ A. u e. ( ordTop ` <_ ) ( P e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) <-> ( P e. RR* /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
42 8 11 41 3bitrd 
 |-  ( ph -> ( F ~~>* P <-> ( P e. RR* /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )