Theorem clnbgrlevtx

Description: The size of the closed neighborhood of a vertex is at most the number of vertices of a graph. (Contributed by AV, 10-May-2025)

	Ref	Expression
Hypothesis	clnbgrlevtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	clnbgrlevtx	$$⊢\left|GClNeighbVtxU\right|\le \left|V\right|$$

Proof

Step	Hyp	Ref	Expression
1		clnbgrlevtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	fvexi	$$⊢V\in \mathrm{V}$$
3	1	clnbgrssvtx	$$⊢GClNeighbVtxU\subseteq V$$
4		hashss	$$⊢\left(V\in \mathrm{V}\wedge GClNeighbVtxU\subseteq V\right)\to \left|GClNeighbVtxU\right|\le \left|V\right|$$
5	2 3 4	mp2an	$$⊢\left|GClNeighbVtxU\right|\le \left|V\right|$$