Definition df-nbgr 29350

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 (see df-clnbgr 47806), a vertex is not a neighbor of itself (see nbgrnself 29376). 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 23106), 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.)

Assertion

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

Distinct variable group:   𝑒,𝑔,𝑛,𝑣

Detailed syntax breakdown of Definition df-nbgr

Step	Hyp	Ref	Expression
1		cnbgr 29349	. 2 class NeighbVtx
2		vg	. . 3 setvar 𝑔
3		vv	. . 3 setvar 𝑣
4		cvv 3480	. . 3 class V
5	2	cv 1539	. . . 4 class 𝑔
6		cvtx 29013	. . . 4 class Vtx
7	5, 6	cfv 6561	. . 3 class (Vtx‘𝑔)
8	3	cv 1539	. . . . . . 7 class 𝑣
9		vn	. . . . . . . 8 setvar 𝑛
10	9	cv 1539	. . . . . . 7 class 𝑛
11	8, 10	cpr 4628	. . . . . 6 class {𝑣, 𝑛}
12		ve	. . . . . . 7 setvar 𝑒
13	12	cv 1539	. . . . . 6 class 𝑒
14	11, 13	wss 3951	. . . . 5 wff {𝑣, 𝑛} ⊆ 𝑒
15		cedg 29064	. . . . . 6 class Edg
16	5, 15	cfv 6561	. . . . 5 class (Edg‘𝑔)
17	14, 12, 16	wrex 3070	. . . 4 wff ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒
18	8	csn 4626	. . . . 5 class {𝑣}
19	7, 18	cdif 3948	. . . 4 class ((Vtx‘𝑔) ∖ {𝑣})
20	17, 9, 19	crab 3436	. . 3 class {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}
21	2, 3, 4, 7, 20	cmpo 7433	. 2 class (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
22	1, 21	wceq 1540	1 wff NeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})

This definition is referenced by:  nbgrprc0  29351  nbgrcl  29352  nbgrval  29353  nbgrnvtx0  29356