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