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 26798
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 21390), 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 26797 . 2 class NeighbVtx
2 vg . . 3 setvar 𝑔
3 vv . . 3 setvar 𝑣
4 cvv 3437 . . 3 class V
52cv 1521 . . . 4 class 𝑔
6 cvtx 26464 . . . 4 class Vtx
75, 6cfv 6225 . . 3 class (Vtx‘𝑔)
83cv 1521 . . . . . . 7 class 𝑣
9 vn . . . . . . . 8 setvar 𝑛
109cv 1521 . . . . . . 7 class 𝑛
118, 10cpr 4474 . . . . . 6 class {𝑣, 𝑛}
12 ve . . . . . . 7 setvar 𝑒
1312cv 1521 . . . . . 6 class 𝑒
1411, 13wss 3859 . . . . 5 wff {𝑣, 𝑛} ⊆ 𝑒
15 cedg 26515 . . . . . 6 class Edg
165, 15cfv 6225 . . . . 5 class (Edg‘𝑔)
1714, 12, 16wrex 3106 . . . 4 wff 𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒
188csn 4472 . . . . 5 class {𝑣}
197, 18cdif 3856 . . . 4 class ((Vtx‘𝑔) ∖ {𝑣})
2017, 9, 19crab 3109 . . 3 class {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}
212, 3, 4, 7, 20cmpo 7018 . 2 class (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
221, 21wceq 1522 1 wff NeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
Colors of variables: wff setvar class
This definition is referenced by:  nbgrprc0  26799  nbgrcl  26800  nbgrval  26801  nbgrnvtx0  26804
  Copyright terms: Public domain W3C validator