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 )