Definition df-nei

Description: Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007)

	Ref	Expression
Assertion	df-nei	|- nei = ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnei	|- nei
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6	5	cpw	|- ~P U. j
7		vy	|- y
8		vg	|- g
9	3	cv	|- x
10	8	cv	|- g
11	9 10	wss	|- x C_ g
12	7	cv	|- y
13	10 12	wss	|- g C_ y
14	11 13	wa	|- ( x C_ g /\ g C_ y )
15	14 8 4	wrex	|- E. g e. j ( x C_ g /\ g C_ y )
16	15 7 6	crab	|- { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) }
17	3 6 16	cmpt	|- ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } )
18	1 2 17	cmpt	|- ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )
19	0 18	wceq	|- nei = ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )