fbasne0

Description: There are no empty filter bases. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

		Ref	Expression
	Assertion	fbasne0	$⊢ F \in fBas (B) \to F \neq \emptyset$

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		simpr1	$⊢ (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 F \neq \emptyset$
6	4 5	syl	$⊢ F \in fBas (B) \to F \neq \emptyset$

Metamath Proof Explorer