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 ‘ 𝐽 ) ‘ 𝑁 ) ↔ 𝑁 ∈ 𝐽 ) )