Metamath Proof Explorer


Theorem 0nelfil

Description: The empty set doesn't belong to a filter. (Contributed by FL, 20-Jul-2007) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion 0nelfil ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 filfbas ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2 0nelfb ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
3 1 2 syl ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )