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

Proof

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