Theorem neival

Description: Value of the set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	neifval.1	|- X = U. J
Assertion	neival	|- ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )

Proof

Step	Hyp	Ref	Expression
1		neifval.1	|- X = U. J
2	1	neifval	|- ( J e. Top -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )
3	2	fveq1d	|- ( J e. Top -> ( ( nei ` J ) ` S ) = ( ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) ` S ) )
4	3	adantr	|- ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = ( ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) ` S ) )
5		eqid	|- ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } )
6		cleq1lem	|- ( x = S -> ( ( x C_ g /\ g C_ v ) <-> ( S C_ g /\ g C_ v ) ) )
7	6	rexbidv	|- ( x = S -> ( E. g e. J ( x C_ g /\ g C_ v ) <-> E. g e. J ( S C_ g /\ g C_ v ) ) )
8	7	rabbidv	|- ( x = S -> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
9	1	topopn	|- ( J e. Top -> X e. J )
10		elpw2g	|- ( X e. J -> ( S e. ~P X <-> S C_ X ) )
11	9 10	syl	|- ( J e. Top -> ( S e. ~P X <-> S C_ X ) )
12	11	biimpar	|- ( ( J e. Top /\ S C_ X ) -> S e. ~P X )
13		pwexg	|- ( X e. J -> ~P X e. _V )
14		rabexg	|- ( ~P X e. _V -> { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } e. _V )
15	9 13 14	3syl	|- ( J e. Top -> { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } e. _V )
16	15	adantr	|- ( ( J e. Top /\ S C_ X ) -> { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } e. _V )
17	5 8 12 16	fvmptd3	|- ( ( J e. Top /\ S C_ X ) -> ( ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
18	4 17	eqtrd	|- ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )