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

Metamath Proof Explorer

Theorem opnssneib

Description: Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007)

Ref Expression
Hypothesis neips.1 
|- X = U. J
Assertion opnssneib 
|- ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )

Proof

Step Hyp Ref Expression
1 neips.1 
 |-  X = U. J
2 simplr 
 |-  ( ( ( S e. J /\ N C_ X ) /\ S C_ N ) -> N C_ X )
3 sseq2 
 |-  ( g = S -> ( S C_ g <-> S C_ S ) )
4 sseq1 
 |-  ( g = S -> ( g C_ N <-> S C_ N ) )
5 3 4 anbi12d 
 |-  ( g = S -> ( ( S C_ g /\ g C_ N ) <-> ( S C_ S /\ S C_ N ) ) )
6 ssid 
 |-  S C_ S
7 6 biantrur 
 |-  ( S C_ N <-> ( S C_ S /\ S C_ N ) )
8 5 7 bitr4di 
 |-  ( g = S -> ( ( S C_ g /\ g C_ N ) <-> S C_ N ) )
9 8 rspcev 
 |-  ( ( S e. J /\ S C_ N ) -> E. g e. J ( S C_ g /\ g C_ N ) )
10 9 adantlr 
 |-  ( ( ( S e. J /\ N C_ X ) /\ S C_ N ) -> E. g e. J ( S C_ g /\ g C_ N ) )
11 2 10 jca 
 |-  ( ( ( S e. J /\ N C_ X ) /\ S C_ N ) -> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) )
12 11 ex 
 |-  ( ( S e. J /\ N C_ X ) -> ( S C_ N -> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
13 12 3adant1 
 |-  ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( S C_ N -> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
14 1 eltopss 
 |-  ( ( J e. Top /\ S e. J ) -> S C_ X )
15 1 isnei 
 |-  ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
16 14 15 syldan 
 |-  ( ( J e. Top /\ S e. J ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
17 16 3adant3 
 |-  ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
18 13 17 sylibrd 
 |-  ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( S C_ N -> N e. ( ( nei ` J ) ` S ) ) )
19 ssnei 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ N )
20 19 ex 
 |-  ( J e. Top -> ( N e. ( ( nei ` J ) ` S ) -> S C_ N ) )
21 20 3ad2ant1 
 |-  ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) -> S C_ N ) )
22 18 21 impbid 
 |-  ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )