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	$⊢ Z = ℤ_{\geq M}$
	Assertion	uzfbas	$⊢ M \in ℤ \to ℤ_{\geq} [Z] \in fBas (Z)$

Proof

Step	Hyp	Ref	Expression
1		uzfbas.1	$⊢ Z = ℤ_{\geq M}$
2	1	uzrest	$⊢ M \in ℤ \to ran ℤ_{\geq} ↾_{𝑡} Z = ℤ_{\geq} [Z]$
3		zfbas	$⊢ ran ℤ_{\geq} \in fBas (ℤ)$
4		0nelfb	$⊢ ran ℤ_{\geq} \in fBas (ℤ) \to \neg \emptyset \in ran ℤ_{\geq}$
5	3 4	ax-mp	$⊢ \neg \emptyset \in ran ℤ_{\geq}$
6		imassrn	$⊢ ℤ_{\geq} [Z] \subseteq ran ℤ_{\geq}$
7	2 6	eqsstrdi	$⊢ M \in ℤ \to ran ℤ_{\geq} ↾_{𝑡} Z \subseteq ran ℤ_{\geq}$
8	7	sseld	$⊢ M \in ℤ \to (\emptyset \in (ran ℤ_{\geq} ↾_{𝑡} Z) \to \emptyset \in ran ℤ_{\geq})$
9	5 8	mtoi	$⊢ M \in ℤ \to \neg \emptyset \in (ran ℤ_{\geq} ↾_{𝑡} Z)$
10		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
11	1 10	eqsstri	$⊢ Z \subseteq ℤ$
12		trfbas2	$⊢ (ran ℤ_{\geq} \in fBas (ℤ) \land Z \subseteq ℤ) \to (ran ℤ_{\geq} ↾_{𝑡} Z \in fBas (Z) \leftrightarrow \neg \emptyset \in (ran ℤ_{\geq} ↾_{𝑡} Z))$
13	3 11 12	mp2an	$⊢ ran ℤ_{\geq} ↾_{𝑡} Z \in fBas (Z) \leftrightarrow \neg \emptyset \in (ran ℤ_{\geq} ↾_{𝑡} Z)$
14	9 13	sylibr	$⊢ M \in ℤ \to ran ℤ_{\geq} ↾_{𝑡} Z \in fBas (Z)$
15	2 14	eqeltrrd	$⊢ M \in ℤ \to ℤ_{\geq} [Z] \in fBas (Z)$