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 e. Top -> ( N e. ( ( nei ` J ) ` N ) <-> N e. J ) )

Proof

Step Hyp Ref Expression
1 neii2
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` N ) ) -> E. x e. J ( N C_ x /\ x C_ N ) )
2 eqss
 |-  ( N = x <-> ( N C_ x /\ x C_ N ) )
3 eleq1a
 |-  ( x e. J -> ( N = x -> N e. J ) )
4 2 3 syl5bir
 |-  ( x e. J -> ( ( N C_ x /\ x C_ N ) -> N e. J ) )
5 4 rexlimiv
 |-  ( E. x e. J ( N C_ x /\ x C_ N ) -> N e. J )
6 1 5 syl
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` N ) ) -> N e. J )
7 6 ex
 |-  ( J e. Top -> ( N e. ( ( nei ` J ) ` N ) -> N e. J ) )
8 ssid
 |-  N C_ N
9 opnneiss
 |-  ( ( J e. Top /\ N e. J /\ N C_ N ) -> N e. ( ( nei ` J ) ` N ) )
10 9 3exp
 |-  ( J e. Top -> ( N e. J -> ( N C_ N -> N e. ( ( nei ` J ) ` N ) ) ) )
11 8 10 mpii
 |-  ( J e. Top -> ( N e. J -> N e. ( ( nei ` J ) ` N ) ) )
12 7 11 impbid
 |-  ( J e. Top -> ( N e. ( ( nei ` J ) ` N ) <-> N e. J ) )