Metamath Proof Explorer


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 Top N nei J S R S N nei J R

Proof

Step Hyp Ref Expression
1 eqid J = J
2 1 neii1 J Top N nei J S N J
3 2 3adant3 J Top N nei J S R S N J
4 neii2 J Top N nei J S g J S g g N
5 4 3adant3 J Top N nei J S R S g J S g g N
6 sstr2 R S S g R g
7 6 anim1d R S S g g N R g g N
8 7 reximdv R S g J S g g N g J R g g N
9 8 3ad2ant3 J Top N nei J S R S g J S g g N g J R g g N
10 5 9 mpd J Top N nei J S R S g J R g g N
11 simp1 J Top N nei J S R S J Top
12 simp3 J Top N nei J S R S R S
13 1 neiss2 J Top N nei J S S J
14 13 3adant3 J Top N nei J S R S S J
15 12 14 sstrd J Top N nei J S R S R J
16 1 isnei J Top R J N nei J R N J g J R g g N
17 11 15 16 syl2anc J Top N nei J S R S N nei J R N J g J R g g N
18 3 10 17 mpbir2and J Top N nei J S R S N nei J R