This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ( ℤ≥ ‘ 𝑥 ) )
11 n0i ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑥 ) → ¬ ( ℤ≥ ‘ 𝑥 ) = ∅ )
12 10 11 syl ⊢ ( 𝑥 ∈ ℤ → ¬ ( ℤ≥ ‘ 𝑥 ) = ∅ )
13 12 nrex ⊢ ¬ ∃ 𝑥 ∈ ℤ ( ℤ≥ ‘ 𝑥 ) = ∅
14 fvelrnb ⊢ ( ℤ≥ Fn ℤ → ( ∅ ∈ ran ℤ≥ ↔ ∃ 𝑥 ∈ ℤ ( ℤ≥ ‘ 𝑥 ) = ∅ ) )
15 5 14 ax-mp ⊢ ( ∅ ∈ ran ℤ≥ ↔ ∃ 𝑥 ∈ ℤ ( ℤ≥ ‘ 𝑥 ) = ∅ )
16 13 15 mtbir ⊢ ¬ ∅ ∈ ran ℤ≥
17 16 nelir ⊢ ∅ ∉ ran ℤ≥
18 uzin2 ⊢ ( ( 𝑥 ∈ ran ℤ≥ ∧ 𝑦 ∈ ran ℤ≥ ) → ( 𝑥 ∩ 𝑦 ) ∈ ran ℤ≥ )
19 vex ⊢ 𝑥 ∈ V
20 19 inex1 ⊢ ( 𝑥 ∩ 𝑦 ) ∈ V
21 20 pwid ⊢ ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 ( 𝑥 ∩ 𝑦 )
22 inelcm ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ ran ℤ≥ ∧ ( 𝑥 ∩ 𝑦 ) ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) → ( ran ℤ≥ ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ )
23 18 21 22 sylancl ⊢ ( ( 𝑥 ∈ ran ℤ≥ ∧ 𝑦 ∈ ran ℤ≥ ) → ( ran ℤ≥ ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ )
24 23 rgen2 ⊢ ∀ 𝑥 ∈ ran ℤ≥ ∀ 𝑦 ∈ ran ℤ≥ ( ran ℤ≥ ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅
25 9 17 24 3pm3.2i ⊢ ( ran ℤ≥ ≠ ∅ ∧ ∅ ∉ ran ℤ≥ ∧ ∀ 𝑥 ∈ ran ℤ≥ ∀ 𝑦 ∈ ran ℤ≥ ( ran ℤ≥ ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ )
26 zex ⊢ ℤ ∈ V
27 isfbas ⊢ ( ℤ ∈ V → ( ran ℤ≥ ∈ ( fBas ‘ ℤ ) ↔ ( ran ℤ≥ ⊆ 𝒫 ℤ ∧ ( ran ℤ≥ ≠ ∅ ∧ ∅ ∉ ran ℤ≥ ∧ ∀ 𝑥 ∈ ran ℤ≥ ∀ 𝑦 ∈ ran ℤ≥ ( ran ℤ≥ ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
28 26 27 ax-mp ⊢ ( ran ℤ≥ ∈ ( fBas ‘ ℤ ) ↔ ( ran ℤ≥ ⊆ 𝒫 ℤ ∧ ( ran ℤ≥ ≠ ∅ ∧ ∅ ∉ ran ℤ≥ ∧ ∀ 𝑥 ∈ ran ℤ≥ ∀ 𝑦 ∈ ran ℤ≥ ( ran ℤ≥ ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) )
29 3 25 28 mpbir2an ⊢ ran ℤ≥ ∈ ( fBas ‘ ℤ )