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 e. ( Fil ` X ) -> F =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | filtop | |- ( F e. ( Fil ` X ) -> X e. F ) |
|
| 2 | 1 | ne0d | |- ( F e. ( Fil ` X ) -> F =/= (/) ) |