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