Metamath Proof Explorer

Theorem 0nnei

Description: The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007)

Ref Expression
Assertion 0nnei ⊢ J ∈ Top ∧ S ≠ ∅ → ¬ ∅ ∈ nei ⁡ J ⁡ S

Proof

Step Hyp Ref Expression
1 ssnei ⊢ J ∈ Top ∧ ∅ ∈ nei ⁡ J ⁡ S → S ⊆ ∅
2 ss0b ⊢ S ⊆ ∅ ↔ S = ∅
3 1 2 sylib ⊢ J ∈ Top ∧ ∅ ∈ nei ⁡ J ⁡ S → S = ∅
4 3 ex ⊢ J ∈ Top → ∅ ∈ nei ⁡ J ⁡ S → S = ∅
5 4 necon3ad ⊢ J ∈ Top → S ≠ ∅ → ¬ ∅ ∈ nei ⁡ J ⁡ S
6 5 imp ⊢ J ∈ Top ∧ S ≠ ∅ → ¬ ∅ ∈ nei ⁡ J ⁡ S