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