Theorem opnneip

Description: An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007)

	Ref	Expression
Assertion	opnneip	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )

Proof

Step	Hyp	Ref	Expression
1		snssi	⊢ ( 𝑃 ∈ 𝑁 → { 𝑃 } ⊆ 𝑁 )
2		opnneiss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ { 𝑃 } ⊆ 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
3	1 2	syl3an3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )