Definition df-clnbgr 47806

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 is the set of all vertices which are connected with this vertex by an edge and the vertex itself (in contrast to an open neighborhood, see df-nbgr 29350). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 47811. 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 47805	. 2 class ClNeighbVtx
2		vg	. . 3 setvar 𝑔
3		vv	. . 3 setvar 𝑣
4		cvv 3480	. . 3 class V
5	2	cv 1539	. . . 4 class 𝑔
6		cvtx 29013	. . . 4 class Vtx
7	5, 6	cfv 6561	. . 3 class (Vtx‘𝑔)
8	3	cv 1539	. . . . 5 class 𝑣
9	8	csn 4626	. . . 4 class {𝑣}
10		vn	. . . . . . . . 9 setvar 𝑛
11	10	cv 1539	. . . . . . . 8 class 𝑛
12	8, 11	cpr 4628	. . . . . . 7 class {𝑣, 𝑛}
13		ve	. . . . . . . 8 setvar 𝑒
14	13	cv 1539	. . . . . . 7 class 𝑒
15	12, 14	wss 3951	. . . . . 6 wff {𝑣, 𝑛} ⊆ 𝑒
16		cedg 29064	. . . . . . 7 class Edg
17	5, 16	cfv 6561	. . . . . 6 class (Edg‘𝑔)
18	15, 13, 17	wrex 3070	. . . . 5 wff ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒
19	18, 10, 7	crab 3436	. . . 4 class {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}
20	9, 19	cun 3949	. . 3 class ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})
21	2, 3, 4, 7, 20	cmpo 7433	. 2 class (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))
22	1, 21	wceq 1540	1 wff ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))

This definition is referenced by:  clnbgrprc0  47807  clnbgrcl  47808  clnbgrval  47809  clnbgrnvtx0  47814