Metamath Proof Explorer

Theorem lmcvg

Description: Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypotheses lmcvg.1 
|- Z = ( ZZ>= ` M )
lmcvg.3 
|- ( ph -> P e. U )
lmcvg.4 
|- ( ph -> M e. ZZ )
lmcvg.5 
|- ( ph -> F ( ~~>t ` J ) P )
lmcvg.6 
|- ( ph -> U e. J )
Assertion lmcvg 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. U )

Proof

Step Hyp Ref Expression
1 lmcvg.1 
 |-  Z = ( ZZ>= ` M )
2 lmcvg.3 
 |-  ( ph -> P e. U )
3 lmcvg.4 
 |-  ( ph -> M e. ZZ )
4 lmcvg.5 
 |-  ( ph -> F ( ~~>t ` J ) P )
5 lmcvg.6 
 |-  ( ph -> U e. J )
6 eleq2 
 |-  ( u = U -> ( P e. u <-> P e. U ) )
7 eleq2 
 |-  ( u = U -> ( ( F ` k ) e. u <-> ( F ` k ) e. U ) )
8 7 rexralbidv 
 |-  ( u = U -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. U ) )
9 6 8 imbi12d 
 |-  ( u = U -> ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) <-> ( P e. U -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. U ) ) )
10 lmrcl 
 |-  ( F ( ~~>t ` J ) P -> J e. Top )
11 4 10 syl 
 |-  ( ph -> J e. Top )
12 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
13 11 12 sylib 
 |-  ( ph -> J e. ( TopOn ` U. J ) )
14 13 1 3 lmbr2 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( U. J ^pm CC ) /\ P e. U. J /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
15 4 14 mpbid 
 |-  ( ph -> ( F e. ( U. J ^pm CC ) /\ P e. U. J /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
16 15 simp3d 
 |-  ( 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 ) ) )
17 simpr 
 |-  ( ( k e. dom F /\ ( F ` k ) e. u ) -> ( F ` k ) e. u )
18 17 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. u )
19 18 reximi 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u )
20 19 imim2i 
 |-  ( ( 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. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) )
21 20 ralimi 
 |-  ( 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. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) )
22 16 21 syl 
 |-  ( ph -> A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) )
23 9 22 5 rspcdva 
 |-  ( ph -> ( P e. U -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. U ) )
24 2 23 mpd 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. U )