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 (see df-clnbgr ), a vertex is not a neighbor of itself (see nbgrnself ). 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 ⁡ g v n ⊆ e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnbgr class NeighbVtx
1 vg setvar g
2 cvv class V
3 vv setvar v
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx ⁡ g
7 vn setvar n
8 3 cv setvar v
9 8 csn class v
10 6 9 cdif class Vtx ⁡ g ∖ v
11 ve setvar e
12 cedg class Edg
13 5 12 cfv class Edg ⁡ g
14 7 cv setvar n
15 8 14 cpr class v n
16 11 cv setvar e
17 15 16 wss wff v n ⊆ e
18 17 11 13 wrex wff ∃ e ∈ Edg ⁡ g v n ⊆ e
19 18 7 10 crab class n ∈ Vtx ⁡ g ∖ v | ∃ e ∈ Edg ⁡ g v n ⊆ e
20 1 3 2 6 19 cmpo class g ∈ V , v ∈ Vtx ⁡ g ⟼ n ∈ Vtx ⁡ g ∖ v | ∃ e ∈ Edg ⁡ g v n ⊆ e
21 0 20 wceq wff NeighbVtx = g ∈ V , v ∈ Vtx ⁡ g ⟼ n ∈ Vtx ⁡ g ∖ v | ∃ e ∈ Edg ⁡ g v n ⊆ e