Theorem 0nnei

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

	Ref	Expression
Assertion	0nnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ≠ ∅ ) → ¬ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ssnei	⊢ ( ( 𝐽 ∈ Top ∧ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ∅ )
2		ss0b	⊢ ( 𝑆 ⊆ ∅ ↔ 𝑆 = ∅ )
3	1 2	sylib	⊢ ( ( 𝐽 ∈ Top ∧ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 = ∅ )
4	3	ex	⊢ ( 𝐽 ∈ Top → ( ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑆 = ∅ ) )
5	4	necon3ad	⊢ ( 𝐽 ∈ Top → ( 𝑆 ≠ ∅ → ¬ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
6	5	imp	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ≠ ∅ ) → ¬ ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )