Metamath Proof Explorer

Theorem opnneiid

Description: Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006)

Ref Expression
Assertion opnneiid ⊢ J ∈ Top → N ∈ nei ⁡ J ⁡ N ↔ N ∈ J

Proof

Step Hyp Ref Expression
1 neii2 ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ N → ∃ x ∈ J N ⊆ x ∧ x ⊆ N
2 eqss ⊢ N = x ↔ N ⊆ x ∧ x ⊆ N
3 eleq1a ⊢ x ∈ J → N = x → N ∈ J
4 2 3 biimtrrid ⊢ x ∈ J → N ⊆ x ∧ x ⊆ N → N ∈ J
5 4 rexlimiv ⊢ ∃ x ∈ J N ⊆ x ∧ x ⊆ N → N ∈ J
6 1 5 syl ⊢ J ∈ Top ∧ N ∈ nei ⁡ J ⁡ N → N ∈ J
7 6 ex ⊢ J ∈ Top → N ∈ nei ⁡ J ⁡ N → N ∈ J
8 ssid ⊢ N ⊆ N
9 opnneiss ⊢ J ∈ Top ∧ N ∈ J ∧ N ⊆ N → N ∈ nei ⁡ J ⁡ N
10 9 3exp ⊢ J ∈ Top → N ∈ J → N ⊆ N → N ∈ nei ⁡ J ⁡ N
11 8 10 mpii ⊢ J ∈ Top → N ∈ J → N ∈ nei ⁡ J ⁡ N
12 7 11 impbid ⊢ J ∈ Top → N ∈ nei ⁡ J ⁡ N ↔ N ∈ J