0nelfb

Description: No filter base contains the empty set. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

		Ref	Expression
	Assertion	0nelfb	$⊢ F \in fBas (B) \to \neg \emptyset \in F$

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ F \in fBas (B) \to B \in dom fBas$
2		isfbas	$⊢ B \in dom fBas \to (F \in fBas (B) \leftrightarrow (F \subseteq 𝒫 B \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)))$
3	1 2	syl	$⊢ F \in fBas (B) \to (F \in fBas (B) \leftrightarrow (F \subseteq 𝒫 B \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)))$
4	3	ibi	$⊢ F \in fBas (B) \to (F \subseteq 𝒫 B \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset))$
5		simpr2	$⊢ (F \subseteq 𝒫 B \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)) \to \emptyset \notin F$
6	4 5	syl	$⊢ F \in fBas (B) \to \emptyset \notin F$
7		df-nel	$⊢ \emptyset \notin F \leftrightarrow \neg \emptyset \in F$
8	6 7	sylib	$⊢ F \in fBas (B) \to \neg \emptyset \in F$

Metamath Proof Explorer