Metamath Proof Explorer

Theorem lmconst

Description: A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypothesis lmconst.2 
|- Z = ( ZZ>= ` M )
Assertion lmconst 
|- ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> ( Z X. { P } ) ( ~~>t ` J ) P )

Proof

Step Hyp Ref Expression
1 lmconst.2 
 |-  Z = ( ZZ>= ` M )
2 simp2 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> P e. X )
3 simp3 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> M e. ZZ )
4 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
5 3 4 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> M e. ( ZZ>= ` M ) )
6 5 1 eleqtrrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> M e. Z )
7 idd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) /\ k e. ( ZZ>= ` M ) ) -> ( P e. u -> P e. u ) )
8 7 ralrimdva 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> ( P e. u -> A. k e. ( ZZ>= ` M ) P e. u ) )
9 fveq2 
 |-  ( j = M -> ( ZZ>= ` j ) = ( ZZ>= ` M ) )
10 9 raleqdv 
 |-  ( j = M -> ( A. k e. ( ZZ>= ` j ) P e. u <-> A. k e. ( ZZ>= ` M ) P e. u ) )
11 10 rspcev 
 |-  ( ( M e. Z /\ A. k e. ( ZZ>= ` M ) P e. u ) -> E. j e. Z A. k e. ( ZZ>= ` j ) P e. u )
12 6 8 11 syl6an 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) P e. u ) )
13 12 ralrimivw 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) P e. u ) )
14 simp1 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> J e. ( TopOn ` X ) )
15 fconst6g 
 |-  ( P e. X -> ( Z X. { P } ) : Z --> X )
16 2 15 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> ( Z X. { P } ) : Z --> X )
17 fvconst2g 
 |-  ( ( P e. X /\ k e. Z ) -> ( ( Z X. { P } ) ` k ) = P )
18 2 17 sylan 
 |-  ( ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) /\ k e. Z ) -> ( ( Z X. { P } ) ` k ) = P )
19 14 1 3 16 18 lmbrf 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> ( ( Z X. { P } ) ( ~~>t ` J ) P <-> ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) P e. u ) ) ) )
20 2 13 19 mpbir2and 
 |-  ( ( J e. ( TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> ( Z X. { P } ) ( ~~>t ` J ) P )