Definition df-nei 12779

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

Assertion

Ref	Expression
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 ) } ) )

Distinct variable group:   g, j, x, y

Detailed syntax breakdown of Definition df-nei

Step	Hyp	Ref	Expression
1		cnei 12778	. 2 class nei
2		vj	. . 3 setvar j
3		ctop 12635	. . 3 class Top
4		vx	. . . 4 setvar x
5	2	cv 1342	. . . . . 6 class j
6	5	cuni 3789	. . . . 5 class U. j
7	6	cpw 3559	. . . 4 class ~P U. j
8	4	cv 1342	. . . . . . . 8 class x
9		vg	. . . . . . . . 9 setvar g
10	9	cv 1342	. . . . . . . 8 class g
11	8, 10	wss 3116	. . . . . . 7 wff x C_ g
12		vy	. . . . . . . . 9 setvar y
13	12	cv 1342	. . . . . . . 8 class y
14	10, 13	wss 3116	. . . . . . 7 wff g C_ y
15	11, 14	wa 103	. . . . . 6 wff ( x C_ g /\ g C_ y )
16	15, 9, 5	wrex 2445	. . . . 5 wff E. g e. j ( x C_ g /\ g C_ y )
17	16, 12, 7	crab 2448	. . . 4 class { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) }
18	4, 7, 17	cmpt 4043	. . 3 class ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } )
19	2, 3, 18	cmpt 4043	. 2 class ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )
20	1, 19	wceq 1343	1 wff nei = ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )

This definition is referenced by:  neifval  12780