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