Definition df-clnbgr 47693

Description: Define the closed neighborhood resp. the class of all neighbors of a vertex (in a graph) and the vertex itself, see definition in section I.1 of [Bollobas] p. 3. The closed neighborhood of a vertex are all vertices which are connected with this vertex by an edge and the vertex itself (in contrast to an open neighborhood, see df-nbgr 29368). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 47698. This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025.)

Assertion

Ref	Expression
df-clnbgr	⊢ ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))

Distinct variable group:   𝑒,𝑔,𝑛,𝑣

Detailed syntax breakdown of Definition df-clnbgr

Step	Hyp	Ref	Expression
1		cclnbgr 47692	. 2 class ClNeighbVtx
2		vg	. . 3 setvar 𝑔
3		vv	. . 3 setvar 𝑣
4		cvv 3488	. . 3 class V
5	2	cv 1536	. . . 4 class 𝑔
6		cvtx 29031	. . . 4 class Vtx
7	5, 6	cfv 6573	. . 3 class (Vtx‘𝑔)
8	3	cv 1536	. . . . 5 class 𝑣
9	8	csn 4648	. . . 4 class {𝑣}
10		vn	. . . . . . . . 9 setvar 𝑛
11	10	cv 1536	. . . . . . . 8 class 𝑛
12	8, 11	cpr 4650	. . . . . . 7 class {𝑣, 𝑛}
13		ve	. . . . . . . 8 setvar 𝑒
14	13	cv 1536	. . . . . . 7 class 𝑒
15	12, 14	wss 3976	. . . . . 6 wff {𝑣, 𝑛} ⊆ 𝑒
16		cedg 29082	. . . . . . 7 class Edg
17	5, 16	cfv 6573	. . . . . 6 class (Edg‘𝑔)
18	15, 13, 17	wrex 3076	. . . . 5 wff ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒
19	18, 10, 7	crab 3443	. . . 4 class {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}
20	9, 19	cun 3974	. . 3 class ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
21	2, 3, 4, 7, 20	cmpo 7450	. 2 class (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))
22	1, 21	wceq 1537	1 wff ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))

This definition is referenced by:  clnbgrprc0  47694  clnbgrcl  47695  clnbgrval  47696  clnbgrnvtx0  47700