Theorem elnei

Description: A point belongs to any of its neighborhoods. Property V_iii of BourbakiTop1 p. I.3. (Contributed by FL, 28-Sep-2006)

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

Proof

Step	Hyp	Ref	Expression
1		ssnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → { 𝑃 } ⊆ 𝑁 )
2	1	3adant2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝐴 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → { 𝑃 } ⊆ 𝑁 )
3		snssg	⊢ ( 𝑃 ∈ 𝐴 → ( 𝑃 ∈ 𝑁 ↔ { 𝑃 } ⊆ 𝑁 ) )
4	3	3ad2ant2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝐴 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( 𝑃 ∈ 𝑁 ↔ { 𝑃 } ⊆ 𝑁 ) )
5	2 4	mpbird	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝐴 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → 𝑃 ∈ 𝑁 )