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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	uzfbas	⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ “ 𝑍 ) ∈ ( fBas ‘ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		uzfbas.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2	1	uzrest	⊢ ( 𝑀 ∈ ℤ → ( ran ℤ≥ ↾t 𝑍 ) = ( ℤ≥ “ 𝑍 ) )
3		zfbas	⊢ ran ℤ≥ ∈ ( fBas ‘ ℤ )
4		0nelfb	⊢ ( ran ℤ≥ ∈ ( fBas ‘ ℤ ) → ¬ ∅ ∈ ran ℤ≥ )
5	3 4	ax-mp	⊢ ¬ ∅ ∈ ran ℤ≥
6		imassrn	⊢ ( ℤ≥ “ 𝑍 ) ⊆ ran ℤ≥
7	2 6	eqsstrdi	⊢ ( 𝑀 ∈ ℤ → ( ran ℤ≥ ↾t 𝑍 ) ⊆ ran ℤ≥ )
8	7	sseld	⊢ ( 𝑀 ∈ ℤ → ( ∅ ∈ ( ran ℤ≥ ↾t 𝑍 ) → ∅ ∈ ran ℤ≥ ) )
9	5 8	mtoi	⊢ ( 𝑀 ∈ ℤ → ¬ ∅ ∈ ( ran ℤ≥ ↾t 𝑍 ) )
10		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
11	1 10	eqsstri	⊢ 𝑍 ⊆ ℤ
12		trfbas2	⊢ ( ( ran ℤ≥ ∈ ( fBas ‘ ℤ ) ∧ 𝑍 ⊆ ℤ ) → ( ( ran ℤ≥ ↾t 𝑍 ) ∈ ( fBas ‘ 𝑍 ) ↔ ¬ ∅ ∈ ( ran ℤ≥ ↾t 𝑍 ) ) )
13	3 11 12	mp2an	⊢ ( ( ran ℤ≥ ↾t 𝑍 ) ∈ ( fBas ‘ 𝑍 ) ↔ ¬ ∅ ∈ ( ran ℤ≥ ↾t 𝑍 ) )
14	9 13	sylibr	⊢ ( 𝑀 ∈ ℤ → ( ran ℤ≥ ↾t 𝑍 ) ∈ ( fBas ‘ 𝑍 ) )
15	2 14	eqeltrrd	⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ “ 𝑍 ) ∈ ( fBas ‘ 𝑍 ) )