This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem neii1

Description: A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007)

Ref Expression
Hypothesis neifval.1 
|- X = U. J
Assertion neii1 
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ X )

Proof

Step Hyp Ref Expression
1 neifval.1 
 |-  X = U. J
2 1 neiss2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ X )
3 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 ) ) ) )
4 simpl 
 |-  ( ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) -> N C_ X )
5 3 4 biimtrdi 
 |-  ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) -> N C_ X ) )
6 5 impancom 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( S C_ X -> N C_ X ) )
7 2 6 mpd 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ X )