This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem filn0

Description: The empty set is not a filter. Remark below Definition 1 of BourbakiTop1 p. I.36. (Contributed by FL, 30-Oct-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		filtop	$⊢ F \in Fil (X) \to X \in F$
2	1	ne0d	$⊢ F \in Fil (X) \to F \neq \emptyset$