Theorem 0nei

Description: The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006)

	Ref	Expression
Assertion	0nei	⊢ ( 𝐽 ∈ Top → ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		0opn	⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
2		opnneiid	⊢ ( 𝐽 ∈ Top → ( ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ ∅ ) ↔ ∅ ∈ 𝐽 ) )
3	1 2	mpbird	⊢ ( 𝐽 ∈ Top → ∅ ∈ ( ( nei ‘ 𝐽 ) ‘ ∅ ) )