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

Metamath Proof Explorer

Theorem neiss2

Description: A set with a neighborhood is a subset of the base set of a topology. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by NM, 12-Feb-2007)

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

Proof

Step Hyp Ref Expression
1 neifval.1 
 |-  X = U. J
2 elfvdm 
 |-  ( N e. ( ( nei ` J ) ` S ) -> S e. dom ( nei ` J ) )
3 2 adantl 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S e. dom ( nei ` J ) )
4 1 neif 
 |-  ( J e. Top -> ( nei ` J ) Fn ~P X )
5 4 fndmd 
 |-  ( J e. Top -> dom ( nei ` J ) = ~P X )
6 5 eleq2d 
 |-  ( J e. Top -> ( S e. dom ( nei ` J ) <-> S e. ~P X ) )
7 6 adantr 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( S e. dom ( nei ` J ) <-> S e. ~P X ) )
8 3 7 mpbid 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S e. ~P X )
9 8 elpwid 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ X )