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 ‘ 𝑋 ) → 𝐹 ≠ ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | filtop | ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 ) | |
2 | 1 | ne0d | ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ ) |