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	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		filtop	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
2	1	ne0d	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )