Metamath Proof Explorer

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=g∈V,v∈Vtx⁡g⟼n∈Vtx⁡g∖v|∃e∈Edg⁡gvn⊆e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnbgr classNeighbVtx
1 vg setvarg
2 cvv classV
3 vv setvarv
4 cvtx classVtx
5 1 cv setvarg
6 5 4 cfv classVtx⁡g
7 vn setvarn
8 3 cv setvarv
9 8 csn classv
10 6 9 cdif classVtx⁡g∖v
11 ve setvare
12 cedg classEdg
13 5 12 cfv classEdg⁡g
14 7 cv setvarn
15 8 14 cpr classvn
16 11 cv setvare
17 15 16 wss wffvn⊆e
18 17 11 13 wrex wff∃e∈Edg⁡gvn⊆e
19 18 7 10 crab classn∈Vtx⁡g∖v|∃e∈Edg⁡gvn⊆e
20 1 3 2 6 19 cmpo classg∈V,v∈Vtx⁡g⟼n∈Vtx⁡g∖v|∃e∈Edg⁡gvn⊆e
21 0 20 wceq wffNeighbVtx=g∈V,v∈Vtx⁡g⟼n∈Vtx⁡g∖v|∃e∈Edg⁡gvn⊆e