Theorem neiss

Description: Any neighborhood of a set S is also a neighborhood of any subset R C_ S . Similar to Proposition 1 of BourbakiTop1 p. I.2. (Contributed by FL, 25-Sep-2006)

	Ref	Expression
Assertion	neiss	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> N e. ( ( nei ` J ) ` R ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- U. J = U. J
2	1	neii1	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ U. J )
3	2	3adant3	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> N C_ U. J )
4		neii2	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
5	4	3adant3	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> E. g e. J ( S C_ g /\ g C_ N ) )
6		sstr2	|- ( R C_ S -> ( S C_ g -> R C_ g ) )
7	6	anim1d	|- ( R C_ S -> ( ( S C_ g /\ g C_ N ) -> ( R C_ g /\ g C_ N ) ) )
8	7	reximdv	|- ( R C_ S -> ( E. g e. J ( S C_ g /\ g C_ N ) -> E. g e. J ( R C_ g /\ g C_ N ) ) )
9	8	3ad2ant3	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> ( E. g e. J ( S C_ g /\ g C_ N ) -> E. g e. J ( R C_ g /\ g C_ N ) ) )
10	5 9	mpd	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> E. g e. J ( R C_ g /\ g C_ N ) )
11		simp1	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> J e. Top )
12		simp3	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> R C_ S )
13	1	neiss2	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ U. J )
14	13	3adant3	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> S C_ U. J )
15	12 14	sstrd	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> R C_ U. J )
16	1	isnei	|- ( ( J e. Top /\ R C_ U. J ) -> ( N e. ( ( nei ` J ) ` R ) <-> ( N C_ U. J /\ E. g e. J ( R C_ g /\ g C_ N ) ) ) )
17	11 15 16	syl2anc	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> ( N e. ( ( nei ` J ) ` R ) <-> ( N C_ U. J /\ E. g e. J ( R C_ g /\ g C_ N ) ) ) )
18	3 10 17	mpbir2and	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> N e. ( ( nei ` J ) ` R ) )