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 26270
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 20950), 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 26269 . 2 class NeighbVtx
2 vg . . 3 setvar 𝑔
3 vv . . 3 setvar 𝑣
4 cvv 3231 . . 3 class V
52cv 1522 . . . 4 class 𝑔
6 cvtx 25919 . . . 4 class Vtx
75, 6cfv 5926 . . 3 class (Vtx‘𝑔)
83cv 1522 . . . . . . 7 class 𝑣
9 vn . . . . . . . 8 setvar 𝑛
109cv 1522 . . . . . . 7 class 𝑛
118, 10cpr 4212 . . . . . 6 class {𝑣, 𝑛}
12 ve . . . . . . 7 setvar 𝑒
1312cv 1522 . . . . . 6 class 𝑒
1411, 13wss 3607 . . . . 5 wff {𝑣, 𝑛} ⊆ 𝑒
15 cedg 25984 . . . . . 6 class Edg
165, 15cfv 5926 . . . . 5 class (Edg‘𝑔)
1714, 12, 16wrex 2942 . . . 4 wff 𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒
188csn 4210 . . . . 5 class {𝑣}
197, 18cdif 3604 . . . 4 class ((Vtx‘𝑔) ∖ {𝑣})
2017, 9, 19crab 2945 . . 3 class {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}
212, 3, 4, 7, 20cmpt2 6692 . 2 class (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
221, 21wceq 1523 1 wff NeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
Colors of variables: wff setvar class
This definition is referenced by:  nbgrprc0  26271  nbgrcl  26272  nbgrclOLD  26273  nbgrval  26274  nbgrnvtx0  26277
  Copyright terms: Public domain W3C validator