Theorem dfclnbgr5

Description: Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiclosed neighborhood. (Contributed by AV, 16-May-2025)

	Ref	Expression
Hypotheses	dfsclnbgr2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	dfsclnbgr2.s	$$⊢S=\left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
	dfsclnbgr2.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	dfclnbgr5	$$⊢N\in V\to GClNeighbVtxN=\left\{N\right\}\cup S$$

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		dfsclnbgr2.s	$$⊢S=\left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
3		dfsclnbgr2.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
4	1 3	dfclnbgr2	$$⊢N\in V\to GClNeighbVtxN=\left\{N\right\}\cup \left\{n\in V|\exists e\in E\left(N\in e\wedge n\in e\right)\right\}$$
5	1 2 3	dfsclnbgr2	$$⊢N\in V\to S=\left\{n\in V|\exists e\in E\left(N\in e\wedge n\in e\right)\right\}$$
6	5	uneq2d	$$⊢N\in V\to \left\{N\right\}\cup S=\left\{N\right\}\cup \left\{n\in V|\exists e\in E\left(N\in e\wedge n\in e\right)\right\}$$
7	4 6	eqtr4d	$$⊢N\in V\to GClNeighbVtxN=\left\{N\right\}\cup S$$