fbasfip

Description: A filter base has the finite intersection property. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	fbasfip	$⊢ F \in fBas (X) \to \neg \emptyset \in fi (F)$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ y \in (𝒫 F \cap Fin) \leftrightarrow (y \in 𝒫 F \land y \in Fin)$
2		elpwi	$⊢ y \in 𝒫 F \to y \subseteq F$
3	2	anim1i	$⊢ (y \in 𝒫 F \land y \in Fin) \to (y \subseteq F \land y \in Fin)$
4	1 3	sylbi	$⊢ y \in (𝒫 F \cap Fin) \to (y \subseteq F \land y \in Fin)$
5		fbssint	$⊢ (F \in fBas (X) \land y \subseteq F \land y \in Fin) \to \exists z \in F z \subseteq ⋂ y$
6	5	3expb	$⊢ (F \in fBas (X) \land (y \subseteq F \land y \in Fin)) \to \exists z \in F z \subseteq ⋂ y$
7	4 6	sylan2	$⊢ (F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \to \exists z \in F z \subseteq ⋂ y$
8		0nelfb	$⊢ F \in fBas (X) \to \neg \emptyset \in F$
9	8	ad2antrr	$⊢ ((F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \land z \in F) \to \neg \emptyset \in F$
10		eleq1	$⊢ z = \emptyset \to (z \in F \leftrightarrow \emptyset \in F)$
11	10	biimpcd	$⊢ z \in F \to (z = \emptyset \to \emptyset \in F)$
12	11	adantl	$⊢ ((F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \land z \in F) \to (z = \emptyset \to \emptyset \in F)$
13	9 12	mtod	$⊢ ((F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \land z \in F) \to \neg z = \emptyset$
14		ss0	$⊢ z \subseteq \emptyset \to z = \emptyset$
15	13 14	nsyl	$⊢ ((F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \land z \in F) \to \neg z \subseteq \emptyset$
16	15	adantrr	$⊢ ((F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \land (z \in F \land z \subseteq ⋂ y)) \to \neg z \subseteq \emptyset$
17		sseq2	$⊢ \emptyset = ⋂ y \to (z \subseteq \emptyset \leftrightarrow z \subseteq ⋂ y)$
18	17	biimprcd	$⊢ z \subseteq ⋂ y \to (\emptyset = ⋂ y \to z \subseteq \emptyset)$
19	18	ad2antll	$⊢ ((F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \land (z \in F \land z \subseteq ⋂ y)) \to (\emptyset = ⋂ y \to z \subseteq \emptyset)$
20	16 19	mtod	$⊢ ((F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \land (z \in F \land z \subseteq ⋂ y)) \to \neg \emptyset = ⋂ y$
21	7 20	rexlimddv	$⊢ (F \in fBas (X) \land y \in (𝒫 F \cap Fin)) \to \neg \emptyset = ⋂ y$
22	21	nrexdv	$⊢ F \in fBas (X) \to \neg \exists y \in (𝒫 F \cap Fin) \emptyset = ⋂ y$
23		0ex	$⊢ \emptyset \in V$
24		elfi	$⊢ (\emptyset \in V \land F \in fBas (X)) \to (\emptyset \in fi (F) \leftrightarrow \exists y \in (𝒫 F \cap Fin) \emptyset = ⋂ y)$
25	23 24	mpan	$⊢ F \in fBas (X) \to (\emptyset \in fi (F) \leftrightarrow \exists y \in (𝒫 F \cap Fin) \emptyset = ⋂ y)$
26	22 25	mtbird	$⊢ F \in fBas (X) \to \neg \emptyset \in fi (F)$

Metamath Proof Explorer

Theorem fbasfip

Proof