Theorem 0nelfil

Description: The empty set doesn't belong to a filter. (Contributed by FL, 20-Jul-2007) (Revised by Mario Carneiro, 28-Jul-2015)

	Ref	Expression
Assertion	0nelfil	$$⊢F\in \mathrm{Fil}\left(X\right)\to \neg \varnothing \in F$$

Proof

Step	Hyp	Ref	Expression
1		filfbas	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\in \mathrm{fBas}\left(X\right)$$
2		0nelfb	$$⊢F\in \mathrm{fBas}\left(X\right)\to \neg \varnothing \in F$$
3	1 2	syl	$$⊢F\in \mathrm{Fil}\left(X\right)\to \neg \varnothing \in F$$