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

Metamath Proof Explorer

Theorem opnneissb

Description: An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006)

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

Proof

Step Hyp Ref Expression
1 neips.1 
 |-  X = U. J
2 1 eltopss 
 |-  ( ( J e. Top /\ N e. J ) -> N C_ X )
3 2 adantr 
 |-  ( ( ( J e. Top /\ N e. J ) /\ ( S C_ X /\ S C_ N ) ) -> N C_ X )
4 ssid 
 |-  N C_ N
5 sseq2 
 |-  ( g = N -> ( S C_ g <-> S C_ N ) )
6 sseq1 
 |-  ( g = N -> ( g C_ N <-> N C_ N ) )
7 5 6 anbi12d 
 |-  ( g = N -> ( ( S C_ g /\ g C_ N ) <-> ( S C_ N /\ N C_ N ) ) )
8 7 rspcev 
 |-  ( ( N e. J /\ ( S C_ N /\ N C_ N ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
9 4 8 mpanr2 
 |-  ( ( N e. J /\ S C_ N ) -> E. g e. J ( S C_ g /\ g C_ N ) )
10 9 ad2ant2l 
 |-  ( ( ( J e. Top /\ N e. J ) /\ ( S C_ X /\ S C_ N ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
11 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 ) ) ) )
12 11 ad2ant2r 
 |-  ( ( ( J e. Top /\ N e. J ) /\ ( S C_ X /\ S C_ N ) ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
13 3 10 12 mpbir2and 
 |-  ( ( ( J e. Top /\ N e. J ) /\ ( S C_ X /\ S C_ N ) ) -> N e. ( ( nei ` J ) ` S ) )
14 13 exp43 
 |-  ( J e. Top -> ( N e. J -> ( S C_ X -> ( S C_ N -> N e. ( ( nei ` J ) ` S ) ) ) ) )
15 14 3imp 
 |-  ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( S C_ N -> N e. ( ( nei ` J ) ` S ) ) )
16 ssnei 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ N )
17 16 ex 
 |-  ( J e. Top -> ( N e. ( ( nei ` J ) ` S ) -> S C_ N ) )
18 17 3ad2ant1 
 |-  ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) -> S C_ N ) )
19 15 18 impbid 
 |-  ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )