Theorem neifval

Description: Value of the neighborhood function on the subsets 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	neifval	|- ( J e. Top -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )

Proof

Step	Hyp	Ref	Expression
1		neifval.1	|- X = U. J
2	1	topopn	|- ( J e. Top -> X e. J )
3		pwexg	|- ( X e. J -> ~P X e. _V )
4		mptexg	|- ( ~P X e. _V -> ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) e. _V )
5	2 3 4	3syl	|- ( J e. Top -> ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) e. _V )
6		unieq	|- ( j = J -> U. j = U. J )
7	6 1	eqtr4di	|- ( j = J -> U. j = X )
8	7	pweqd	|- ( j = J -> ~P U. j = ~P X )
9		rexeq	|- ( j = J -> ( E. g e. j ( x C_ g /\ g C_ v ) <-> E. g e. J ( x C_ g /\ g C_ v ) ) )
10	8 9	rabeqbidv	|- ( j = J -> { v e. ~P U. j | E. g e. j ( x C_ g /\ g C_ v ) } = { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } )
11	8 10	mpteq12dv	|- ( j = J -> ( x e. ~P U. j |-> { v e. ~P U. j | 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 ) } ) )
12		df-nei	|- nei = ( j e. Top |-> ( x e. ~P U. j |-> { v e. ~P U. j | E. g e. j ( x C_ g /\ g C_ v ) } ) )
13	11 12	fvmptg	|- ( ( J e. Top /\ ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) e. _V ) -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )
14	5 13	mpdan	|- ( J e. Top -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )