# Metamath Proof Explorer

## Theorem zfbas

Description: The set of upper sets of integers is a filter base on ZZ , which corresponds to convergence of sequences on ZZ . (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion zfbas $⊢ ran ⁡ ℤ ≥ ∈ fBas ⁡ ℤ$

### Proof

Step Hyp Ref Expression
1 uzf $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ$
2 frn $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ → ran ⁡ ℤ ≥ ⊆ 𝒫 ℤ$
3 1 2 ax-mp $⊢ ran ⁡ ℤ ≥ ⊆ 𝒫 ℤ$
4 ffn $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ → ℤ ≥ Fn ℤ$
5 1 4 ax-mp $⊢ ℤ ≥ Fn ℤ$
6 1z $⊢ 1 ∈ ℤ$
7 fnfvelrn $⊢ ℤ ≥ Fn ℤ ∧ 1 ∈ ℤ → ℤ ≥ 1 ∈ ran ⁡ ℤ ≥$
8 5 6 7 mp2an $⊢ ℤ ≥ 1 ∈ ran ⁡ ℤ ≥$
9 8 ne0ii $⊢ ran ⁡ ℤ ≥ ≠ ∅$
10 uzid $⊢ x ∈ ℤ → x ∈ ℤ ≥ x$
11 n0i $⊢ x ∈ ℤ ≥ x → ¬ ℤ ≥ x = ∅$
12 10 11 syl $⊢ x ∈ ℤ → ¬ ℤ ≥ x = ∅$
13 12 nrex $⊢ ¬ ∃ x ∈ ℤ ℤ ≥ x = ∅$
14 fvelrnb $⊢ ℤ ≥ Fn ℤ → ∅ ∈ ran ⁡ ℤ ≥ ↔ ∃ x ∈ ℤ ℤ ≥ x = ∅$
15 5 14 ax-mp $⊢ ∅ ∈ ran ⁡ ℤ ≥ ↔ ∃ x ∈ ℤ ℤ ≥ x = ∅$
16 13 15 mtbir $⊢ ¬ ∅ ∈ ran ⁡ ℤ ≥$
17 16 nelir $⊢ ∅ ∉ ran ⁡ ℤ ≥$
18 uzin2 $⊢ x ∈ ran ⁡ ℤ ≥ ∧ y ∈ ran ⁡ ℤ ≥ → x ∩ y ∈ ran ⁡ ℤ ≥$
19 vex $⊢ x ∈ V$
20 19 inex1 $⊢ x ∩ y ∈ V$
21 20 pwid $⊢ x ∩ y ∈ 𝒫 x ∩ y$
22 inelcm $⊢ x ∩ y ∈ ran ⁡ ℤ ≥ ∧ x ∩ y ∈ 𝒫 x ∩ y → ran ⁡ ℤ ≥ ∩ 𝒫 x ∩ y ≠ ∅$
23 18 21 22 sylancl $⊢ x ∈ ran ⁡ ℤ ≥ ∧ y ∈ ran ⁡ ℤ ≥ → ran ⁡ ℤ ≥ ∩ 𝒫 x ∩ y ≠ ∅$
24 23 rgen2 $⊢ ∀ x ∈ ran ⁡ ℤ ≥ ∀ y ∈ ran ⁡ ℤ ≥ ran ⁡ ℤ ≥ ∩ 𝒫 x ∩ y ≠ ∅$
25 9 17 24 3pm3.2i $⊢ ran ⁡ ℤ ≥ ≠ ∅ ∧ ∅ ∉ ran ⁡ ℤ ≥ ∧ ∀ x ∈ ran ⁡ ℤ ≥ ∀ y ∈ ran ⁡ ℤ ≥ ran ⁡ ℤ ≥ ∩ 𝒫 x ∩ y ≠ ∅$
26 zex $⊢ ℤ ∈ V$
27 isfbas $⊢ ℤ ∈ V → ran ⁡ ℤ ≥ ∈ fBas ⁡ ℤ ↔ ran ⁡ ℤ ≥ ⊆ 𝒫 ℤ ∧ ran ⁡ ℤ ≥ ≠ ∅ ∧ ∅ ∉ ran ⁡ ℤ ≥ ∧ ∀ x ∈ ran ⁡ ℤ ≥ ∀ y ∈ ran ⁡ ℤ ≥ ran ⁡ ℤ ≥ ∩ 𝒫 x ∩ y ≠ ∅$
28 26 27 ax-mp $⊢ ran ⁡ ℤ ≥ ∈ fBas ⁡ ℤ ↔ ran ⁡ ℤ ≥ ⊆ 𝒫 ℤ ∧ ran ⁡ ℤ ≥ ≠ ∅ ∧ ∅ ∉ ran ⁡ ℤ ≥ ∧ ∀ x ∈ ran ⁡ ℤ ≥ ∀ y ∈ ran ⁡ ℤ ≥ ran ⁡ ℤ ≥ ∩ 𝒫 x ∩ y ≠ ∅$
29 3 25 28 mpbir2an $⊢ ran ⁡ ℤ ≥ ∈ fBas ⁡ ℤ$