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 ‘ ℤ )