Metamath Proof Explorer


Theorem neii2

Description: Property of a neighborhood. (Contributed by NM, 12-Feb-2007)

Ref Expression
Assertion neii2 J Top N nei J S g J S g g N

Proof

Step Hyp Ref Expression
1 eqid J = J
2 1 neiss2 J Top N nei J S S J
3 1 isnei J Top S J N nei J S N J g J S g g N
4 simpr N J g J S g g N g J S g g N
5 3 4 syl6bi J Top S J N nei J S g J S g g N
6 5 impancom J Top N nei J S S J g J S g g N
7 2 6 mpd J Top N nei J S g J S g g N