Definition df-nbgr

Description: Define the (open)neighborhood resp. the class of all neighbors of a vertex (in a graph), see definition in section I.1 of Bollobas p. 3 or definition in section 1.1 of Diestel p. 3. The neighborhood/neighbors of a vertex are all (other) vertices which are connected with this vertex by an edge. In contrast to a closed neighborhood, a vertex is not a neighbor of itself. This definition is applicable even for arbitrary hypergraphs.

Remark: To distinguish this definition from other definitions for neighborhoods resp. neighbors (e.g., nei in Topology, see df-nei ), the suffix Vtx is added to the class constant NeighbVtx . (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017) (Revised by AV, 24-Oct-2020)

	Ref	Expression
Assertion	df-nbgr	⊢ NeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnbgr	⊢ NeighbVtx
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cvtx	⊢ Vtx
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Vtx ‘ 𝑔 )
7		vn	⊢ 𝑛
8	3	cv	⊢ 𝑣
9	8	csn	⊢ { 𝑣 }
10	6 9	cdif	⊢ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } )
11		ve	⊢ 𝑒
12		cedg	⊢ Edg
13	5 12	cfv	⊢ ( Edg ‘ 𝑔 )
14	7	cv	⊢ 𝑛
15	8 14	cpr	⊢ { 𝑣 , 𝑛 }
16	11	cv	⊢ 𝑒
17	15 16	wss	⊢ { 𝑣 , 𝑛 } ⊆ 𝑒
18	17 11 13	wrex	⊢ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒
19	18 7 10	crab	⊢ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 }
20	1 3 2 6 19	cmpo	⊢ ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )
21	0 20	wceq	⊢ NeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )