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 )