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 ( 𝐽 ∈ Top → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑁 ) ↔ 𝑁𝐽 ) )

Proof

Step Hyp Ref Expression
1 neii2 ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑁 ) ) → ∃ 𝑥𝐽 ( 𝑁𝑥𝑥𝑁 ) )
2 eqss ( 𝑁 = 𝑥 ↔ ( 𝑁𝑥𝑥𝑁 ) )
3 eleq1a ( 𝑥𝐽 → ( 𝑁 = 𝑥𝑁𝐽 ) )
4 2 3 syl5bir ( 𝑥𝐽 → ( ( 𝑁𝑥𝑥𝑁 ) → 𝑁𝐽 ) )
5 4 rexlimiv ( ∃ 𝑥𝐽 ( 𝑁𝑥𝑥𝑁 ) → 𝑁𝐽 )
6 1 5 syl ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑁 ) ) → 𝑁𝐽 )
7 6 ex ( 𝐽 ∈ Top → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑁 ) → 𝑁𝐽 ) )
8 ssid 𝑁𝑁
9 opnneiss ( ( 𝐽 ∈ Top ∧ 𝑁𝐽𝑁𝑁 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑁 ) )
10 9 3exp ( 𝐽 ∈ Top → ( 𝑁𝐽 → ( 𝑁𝑁𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑁 ) ) ) )
11 8 10 mpii ( 𝐽 ∈ Top → ( 𝑁𝐽𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑁 ) ) )
12 7 11 impbid ( 𝐽 ∈ Top → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑁 ) ↔ 𝑁𝐽 ) )