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 ) )