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 𝑍 = ( ℤ𝑀 )
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 ‘ 𝑍 ) )