Theorem clnbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has an empty closed neighborhood in G . (Contributed by AV, 8-May-2025)

	Ref	Expression
Hypothesis	clnbgrel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	clnbgrnvtx0	$$⊢X\notin V\to GClNeighbVtxX=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		clnbgrel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		csbfv	$$⊢⦋G/g⦌\mathrm{Vtx}\left(g\right)=\mathrm{Vtx}\left(G\right)$$
3	1 2	eqtr4i	$$⊢V=⦋G/g⦌\mathrm{Vtx}\left(g\right)$$
4		neleq2	$$⊢V=⦋G/g⦌\mathrm{Vtx}\left(g\right)\to \left(X\notin V\leftrightarrow X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)\right)$$
5	3 4	ax-mp	$$⊢X\notin V\leftrightarrow X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)$$
6	5	biimpi	$$⊢X\notin V\to X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)$$
7	6	olcd	$$⊢X\notin V\to \left(G\notin \mathrm{V}\vee X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)\right)$$
8		df-clnbgr	$$⊢ClNeighbVtx=\left(g\in \mathrm{V},v\in \mathrm{Vtx}\left(g\right)⟼\left\{v\right\}\cup \left\{n\in \mathrm{Vtx}\left(g\right)|\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\right\}\right)$$
9	8	mpoxneldm	$$⊢\left(G\notin \mathrm{V}\vee X\notin ⦋G/g⦌\mathrm{Vtx}\left(g\right)\right)\to GClNeighbVtxX=\varnothing$$
10	7 9	syl	$$⊢X\notin V\to GClNeighbVtxX=\varnothing$$