Theorem neiuni

Description: The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007) (Revised by Mario Carneiro, 9-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		tpnei.1	|- X = U. J
2	1	tpnei	|- ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )
3	2	biimpa	|- ( ( J e. Top /\ S C_ X ) -> X e. ( ( nei ` J ) ` S ) )
4		elssuni	|- ( X e. ( ( nei ` J ) ` S ) -> X C_ U. ( ( nei ` J ) ` S ) )
5	3 4	syl	|- ( ( J e. Top /\ S C_ X ) -> X C_ U. ( ( nei ` J ) ` S ) )
6	1	neii1	|- ( ( J e. Top /\ x e. ( ( nei ` J ) ` S ) ) -> x C_ X )
7	6	ex	|- ( J e. Top -> ( x e. ( ( nei ` J ) ` S ) -> x C_ X ) )
8	7	adantr	|- ( ( J e. Top /\ S C_ X ) -> ( x e. ( ( nei ` J ) ` S ) -> x C_ X ) )
9	8	ralrimiv	|- ( ( J e. Top /\ S C_ X ) -> A. x e. ( ( nei ` J ) ` S ) x C_ X )
10		unissb	|- ( U. ( ( nei ` J ) ` S ) C_ X <-> A. x e. ( ( nei ` J ) ` S ) x C_ X )
11	9 10	sylibr	|- ( ( J e. Top /\ S C_ X ) -> U. ( ( nei ` J ) ` S ) C_ X )
12	5 11	eqssd	|- ( ( J e. Top /\ S C_ X ) -> X = U. ( ( nei ` J ) ` S ) )