Metamath Proof Explorer


Theorem uzfbas

Description: The set of upper sets of integers based at a point in a fixed upper integer set like NN is a filter base on NN , which corresponds to convergence of sequences on NN . (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypothesis uzfbas.1
|- Z = ( ZZ>= ` M )
Assertion uzfbas
|- ( M e. ZZ -> ( ZZ>= " Z ) e. ( fBas ` Z ) )

Proof

Step Hyp Ref Expression
1 uzfbas.1
 |-  Z = ( ZZ>= ` M )
2 1 uzrest
 |-  ( M e. ZZ -> ( ran ZZ>= |`t Z ) = ( ZZ>= " Z ) )
3 zfbas
 |-  ran ZZ>= e. ( fBas ` ZZ )
4 0nelfb
 |-  ( ran ZZ>= e. ( fBas ` ZZ ) -> -. (/) e. ran ZZ>= )
5 3 4 ax-mp
 |-  -. (/) e. ran ZZ>=
6 imassrn
 |-  ( ZZ>= " Z ) C_ ran ZZ>=
7 2 6 eqsstrdi
 |-  ( M e. ZZ -> ( ran ZZ>= |`t Z ) C_ ran ZZ>= )
8 7 sseld
 |-  ( M e. ZZ -> ( (/) e. ( ran ZZ>= |`t Z ) -> (/) e. ran ZZ>= ) )
9 5 8 mtoi
 |-  ( M e. ZZ -> -. (/) e. ( ran ZZ>= |`t Z ) )
10 uzssz
 |-  ( ZZ>= ` M ) C_ ZZ
11 1 10 eqsstri
 |-  Z C_ ZZ
12 trfbas2
 |-  ( ( ran ZZ>= e. ( fBas ` ZZ ) /\ Z C_ ZZ ) -> ( ( ran ZZ>= |`t Z ) e. ( fBas ` Z ) <-> -. (/) e. ( ran ZZ>= |`t Z ) ) )
13 3 11 12 mp2an
 |-  ( ( ran ZZ>= |`t Z ) e. ( fBas ` Z ) <-> -. (/) e. ( ran ZZ>= |`t Z ) )
14 9 13 sylibr
 |-  ( M e. ZZ -> ( ran ZZ>= |`t Z ) e. ( fBas ` Z ) )
15 2 14 eqeltrrd
 |-  ( M e. ZZ -> ( ZZ>= " Z ) e. ( fBas ` Z ) )