This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Vtx (G)$
	Assertion	clnbgrlevtx	$⊢ \|G ClNeighbVtx U\| \leq \|V\|$

Step	Hyp	Ref	Expression
1		clnbgrlevtx.v	$⊢ V = Vtx (G)$
2	1	fvexi	$⊢ V \in V$
3	1	clnbgrssvtx	$⊢ G ClNeighbVtx U \subseteq V$
4		hashss	$⊢ (V \in V \land G ClNeighbVtx U \subseteq V) \to \|G ClNeighbVtx U\| \leq \|V\|$
5	2 3 4	mp2an	$⊢ \|G ClNeighbVtx U\| \leq \|V\|$