This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )