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 ℤ_{\geq} \in fBas (ℤ)$

Proof

Step	Hyp	Ref	Expression
1		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
2		frn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ran ℤ_{\geq} \subseteq 𝒫 ℤ$
3	1 2	ax-mp	$⊢ ran ℤ_{\geq} \subseteq 𝒫 ℤ$
4		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
5	1 4	ax-mp	$⊢ ℤ_{\geq} Fn ℤ$
6		1z	$⊢ 1 \in ℤ$
7		fnfvelrn	$⊢ (ℤ_{\geq} Fn ℤ \land 1 \in ℤ) \to ℤ_{\geq 1} \in ran ℤ_{\geq}$
8	5 6 7	mp2an	$⊢ ℤ_{\geq 1} \in ran ℤ_{\geq}$
9	8	ne0ii	$⊢ ran ℤ_{\geq} \neq \emptyset$
10		uzid	$⊢ x \in ℤ \to x \in ℤ_{\geq x}$
11		n0i	$⊢ x \in ℤ_{\geq x} \to \neg ℤ_{\geq x} = \emptyset$
12	10 11	syl	$⊢ x \in ℤ \to \neg ℤ_{\geq x} = \emptyset$
13	12	nrex	$⊢ \neg \exists x \in ℤ ℤ_{\geq x} = \emptyset$
14		fvelrnb	$⊢ ℤ_{\geq} Fn ℤ \to (\emptyset \in ran ℤ_{\geq} \leftrightarrow \exists x \in ℤ ℤ_{\geq x} = \emptyset)$
15	5 14	ax-mp	$⊢ \emptyset \in ran ℤ_{\geq} \leftrightarrow \exists x \in ℤ ℤ_{\geq x} = \emptyset$
16	13 15	mtbir	$⊢ \neg \emptyset \in ran ℤ_{\geq}$
17	16	nelir	$⊢ \emptyset \notin ran ℤ_{\geq}$
18		uzin2	$⊢ (x \in ran ℤ_{\geq} \land y \in ran ℤ_{\geq}) \to x \cap y \in ran ℤ_{\geq}$
19		vex	$⊢ x \in V$
20	19	inex1	$⊢ x \cap y \in V$
21	20	pwid	$⊢ x \cap y \in 𝒫 (x \cap y)$
22		inelcm	$⊢ (x \cap y \in ran ℤ_{\geq} \land x \cap y \in 𝒫 (x \cap y)) \to ran ℤ_{\geq} \cap 𝒫 (x \cap y) \neq \emptyset$
23	18 21 22	sylancl	$⊢ (x \in ran ℤ_{\geq} \land y \in ran ℤ_{\geq}) \to ran ℤ_{\geq} \cap 𝒫 (x \cap y) \neq \emptyset$
24	23	rgen2	$⊢ \forall x \in ran ℤ_{\geq} \forall y \in ran ℤ_{\geq} ran ℤ_{\geq} \cap 𝒫 (x \cap y) \neq \emptyset$
25	9 17 24	3pm3.2i	$⊢ (ran ℤ_{\geq} \neq \emptyset \land \emptyset \notin ran ℤ_{\geq} \land \forall x \in ran ℤ_{\geq} \forall y \in ran ℤ_{\geq} ran ℤ_{\geq} \cap 𝒫 (x \cap y) \neq \emptyset)$
26		zex	$⊢ ℤ \in V$
27		isfbas	$⊢ ℤ \in V \to (ran ℤ_{\geq} \in fBas (ℤ) \leftrightarrow (ran ℤ_{\geq} \subseteq 𝒫 ℤ \land (ran ℤ_{\geq} \neq \emptyset \land \emptyset \notin ran ℤ_{\geq} \land \forall x \in ran ℤ_{\geq} \forall y \in ran ℤ_{\geq} ran ℤ_{\geq} \cap 𝒫 (x \cap y) \neq \emptyset)))$
28	26 27	ax-mp	$⊢ ran ℤ_{\geq} \in fBas (ℤ) \leftrightarrow (ran ℤ_{\geq} \subseteq 𝒫 ℤ \land (ran ℤ_{\geq} \neq \emptyset \land \emptyset \notin ran ℤ_{\geq} \land \forall x \in ran ℤ_{\geq} \forall y \in ran ℤ_{\geq} ran ℤ_{\geq} \cap 𝒫 (x \cap y) \neq \emptyset))$
29	3 25 28	mpbir2an	$⊢ ran ℤ_{\geq} \in fBas (ℤ)$

Metamath Proof Explorer

Theorem zfbas

Proof