Metamath Proof Explorer

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 ⊢ J ∈ Top ∧ P ∈ A ∧ N ∈ nei ⁡ J ⁡ P → P ∈ N

Proof

Step Hyp Ref Expression
1 ssnei ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ P → P ⊆ N
2 1 3adant2 ⊢ J ∈ Top ∧ P ∈ A ∧ N ∈ nei ⁡ J ⁡ P → P ⊆ N
3 snssg ⊢ P ∈ A → P ∈ N ↔ P ⊆ N
4 3 3ad2ant2 ⊢ J ∈ Top ∧ P ∈ A ∧ N ∈ nei ⁡ J ⁡ P → P ∈ N ↔ P ⊆ N
5 2 4 mpbird ⊢ J ∈ Top ∧ P ∈ A ∧ N ∈ nei ⁡ J ⁡ P → P ∈ N