Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-nbgr Structured version   Visualization version   GIF version

Definition df-nbgr 40554
 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 20712), 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 40550 . 2 class NeighbVtx
2 vg . . 3 setvar 𝑔
3 vv . . 3 setvar 𝑣
4 cvv 3173 . . 3 class V
52cv 1474 . . . 4 class 𝑔
6 cvtx 25673 . . . 4 class Vtx
75, 6cfv 5804 . . 3 class (Vtx‘𝑔)
83cv 1474 . . . . . . 7 class 𝑣
9 vn . . . . . . . 8 setvar 𝑛
109cv 1474 . . . . . . 7 class 𝑛
118, 10cpr 4127 . . . . . 6 class {𝑣, 𝑛}
12 ve . . . . . . 7 setvar 𝑒
1312cv 1474 . . . . . 6 class 𝑒
1411, 13wss 3540 . . . . 5 wff {𝑣, 𝑛} ⊆ 𝑒
15 cedga 25792 . . . . . 6 class Edg
165, 15cfv 5804 . . . . 5 class (Edg‘𝑔)
1714, 12, 16wrex 2897 . . . 4 wff 𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒
188csn 4125 . . . . 5 class {𝑣}
197, 18cdif 3537 . . . 4 class ((Vtx‘𝑔) ∖ {𝑣})
2017, 9, 19crab 2900 . . 3 class {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}
212, 3, 4, 7, 20cmpt2 6551 . 2 class (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
221, 21wceq 1475 1 wff NeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
 Colors of variables: wff setvar class This definition is referenced by:  nbgrprc0  40555  nbgrcl  40559  nbgrval  40560  nbgrnvtx0  40563
 Copyright terms: Public domain W3C validator