MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nbgr Structured version   Visualization version   GIF version

Definition df-nbgr 26115
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 20812), 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
StepHypRef Expression
1 cnbgr 26111 . 2 class NeighbVtx
2 vg . . 3 setvar 𝑔
3 vv . . 3 setvar 𝑣
4 cvv 3186 . . 3 class V
52cv 1479 . . . 4 class 𝑔
6 cvtx 25774 . . . 4 class Vtx
75, 6cfv 5847 . . 3 class (Vtx‘𝑔)
83cv 1479 . . . . . . 7 class 𝑣
9 vn . . . . . . . 8 setvar 𝑛
109cv 1479 . . . . . . 7 class 𝑛
118, 10cpr 4150 . . . . . 6 class {𝑣, 𝑛}
12 ve . . . . . . 7 setvar 𝑒
1312cv 1479 . . . . . 6 class 𝑒
1411, 13wss 3555 . . . . 5 wff {𝑣, 𝑛} ⊆ 𝑒
15 cedg 25839 . . . . . 6 class Edg
165, 15cfv 5847 . . . . 5 class (Edg‘𝑔)
1714, 12, 16wrex 2908 . . . 4 wff 𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒
188csn 4148 . . . . 5 class {𝑣}
197, 18cdif 3552 . . . 4 class ((Vtx‘𝑔) ∖ {𝑣})
2017, 9, 19crab 2911 . . 3 class {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}
212, 3, 4, 7, 20cmpt2 6606 . 2 class (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
221, 21wceq 1480 1 wff NeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
Colors of variables: wff setvar class
This definition is referenced by:  nbgrprc0  26116  nbgrcl  26120  nbgrval  26121  nbgrnvtx0  26124
  Copyright terms: Public domain W3C validator