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 JTopNneiJNNJ

Proof

Step Hyp Ref Expression
1 neii2 JTopNneiJNxJNxxN
2 eqss N=xNxxN
3 eleq1a xJN=xNJ
4 2 3 syl5bir xJNxxNNJ
5 4 rexlimiv xJNxxNNJ
6 1 5 syl JTopNneiJNNJ
7 6 ex JTopNneiJNNJ
8 ssid NN
9 opnneiss JTopNJNNNneiJN
10 9 3exp JTopNJNNNneiJN
11 8 10 mpii JTopNJNneiJN
12 7 11 impbid JTopNneiJNNJ