Theorem tpnei

Description: The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss . (Contributed by FL, 2-Oct-2006)

	Ref	Expression
Hypothesis	tpnei.1	|- X = U. J
Assertion	tpnei	|- ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )

Proof

Step	Hyp	Ref	Expression
1		tpnei.1	|- X = U. J
2	1	topopn	|- ( J e. Top -> X e. J )
3		opnneiss	|- ( ( J e. Top /\ X e. J /\ S C_ X ) -> X e. ( ( nei ` J ) ` S ) )
4	3	3exp	|- ( J e. Top -> ( X e. J -> ( S C_ X -> X e. ( ( nei ` J ) ` S ) ) ) )
5	2 4	mpd	|- ( J e. Top -> ( S C_ X -> X e. ( ( nei ` J ) ` S ) ) )
6		ssnei	|- ( ( J e. Top /\ X e. ( ( nei ` J ) ` S ) ) -> S C_ X )
7	6	ex	|- ( J e. Top -> ( X e. ( ( nei ` J ) ` S ) -> S C_ X ) )
8	5 7	impbid	|- ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )