Definition df-clnbgr

Description: Define the closedneighborhood 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 ). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 . This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclnbgr	⊢ ClNeighbVtx
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cvtx	⊢ Vtx
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Vtx ‘ 𝑔 )
7	3	cv	⊢ 𝑣
8	7	csn	⊢ { 𝑣 }
9		vn	⊢ 𝑛
10		ve	⊢ 𝑒
11		cedg	⊢ Edg
12	5 11	cfv	⊢ ( Edg ‘ 𝑔 )
13	9	cv	⊢ 𝑛
14	7 13	cpr	⊢ { 𝑣 , 𝑛 }
15	10	cv	⊢ 𝑒
16	14 15	wss	⊢ { 𝑣 , 𝑛 } ⊆ 𝑒
17	16 10 12	wrex	⊢ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒
18	17 9 6	crab	⊢ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 }
19	8 18	cun	⊢ ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } )
20	1 3 2 6 19	cmpo	⊢ ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) )
21	0 20	wceq	⊢ ClNeighbVtx = ( 𝑔 ∈ V , 𝑣 ∈ ( Vtx ‘ 𝑔 ) ↦ ( { 𝑣 } ∪ { 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) )