This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrid ⊢ ( 𝑥 ∈ 𝐽 → ( ( 𝑁 ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑁 ) → 𝑁 ∈ 𝐽 ) )
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 ‘ 𝐽 ) ‘ 𝑁 ) ↔ 𝑁 ∈ 𝐽 ) )