Metamath Proof Explorer

Theorem lmlim

Description: Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on CC on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017)

Ref Expression
Hypotheses lmlim.j 
|- J e. ( TopOn ` Y )
lmlim.f 
|- ( ph -> F : NN --> X )
lmlim.p 
|- ( ph -> P e. X )
lmlim.t 
|- ( J |`t X ) = ( ( TopOpen ` CCfld ) |`t X )
lmlim.x 
|- X C_ CC
Assertion lmlim 
|- ( ph -> ( F ( ~~>t ` J ) P <-> F ~~> P ) )

Proof

Step Hyp Ref Expression
1 lmlim.j 
 |-  J e. ( TopOn ` Y )
2 lmlim.f 
 |-  ( ph -> F : NN --> X )
3 lmlim.p 
 |-  ( ph -> P e. X )
4 lmlim.t 
 |-  ( J |`t X ) = ( ( TopOpen ` CCfld ) |`t X )
5 lmlim.x 
 |-  X C_ CC
6 eqid 
 |-  ( J |`t X ) = ( J |`t X )
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 cnex 
 |-  CC e. _V
9 8 a1i 
 |-  ( ph -> CC e. _V )
10 5 a1i 
 |-  ( ph -> X C_ CC )
11 9 10 ssexd 
 |-  ( ph -> X e. _V )
12 1 topontopi 
 |-  J e. Top
13 12 a1i 
 |-  ( ph -> J e. Top )
14 1z 
 |-  1 e. ZZ
15 14 a1i 
 |-  ( ph -> 1 e. ZZ )
16 6 7 11 13 3 15 2 lmss 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> F ( ~~>t ` ( J |`t X ) ) P ) )
17 4 fveq2i 
 |-  ( ~~>t ` ( J |`t X ) ) = ( ~~>t ` ( ( TopOpen ` CCfld ) |`t X ) )
18 17 breqi 
 |-  ( F ( ~~>t ` ( J |`t X ) ) P <-> F ( ~~>t ` ( ( TopOpen ` CCfld ) |`t X ) ) P )
19 18 a1i 
 |-  ( ph -> ( F ( ~~>t ` ( J |`t X ) ) P <-> F ( ~~>t ` ( ( TopOpen ` CCfld ) |`t X ) ) P ) )
20 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t X ) = ( ( TopOpen ` CCfld ) |`t X )
21 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
22 21 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
23 22 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
24 20 7 11 23 3 15 2 lmss 
 |-  ( ph -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) P <-> F ( ~~>t ` ( ( TopOpen ` CCfld ) |`t X ) ) P ) )
25 fss 
 |-  ( ( F : NN --> X /\ X C_ CC ) -> F : NN --> CC )
26 2 5 25 sylancl 
 |-  ( ph -> F : NN --> CC )
27 21 7 lmclimf 
 |-  ( ( 1 e. ZZ /\ F : NN --> CC ) -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) P <-> F ~~> P ) )
28 14 26 27 sylancr 
 |-  ( ph -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) P <-> F ~~> P ) )
29 24 28 bitr3d 
 |-  ( ph -> ( F ( ~~>t ` ( ( TopOpen ` CCfld ) |`t X ) ) P <-> F ~~> P ) )
30 16 19 29 3bitrd 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> F ~~> P ) )