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