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

Metamath Proof Explorer

Theorem clnbgrn0

Description: The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025)

		Ref	Expression
	Hypothesis	clnbgrn0.v	$⊢ V = Vtx (G)$
	Assertion	clnbgrn0	$⊢ N \in V \to G ClNeighbVtx N \neq \emptyset$

Step	Hyp	Ref	Expression
1		clnbgrn0.v	$⊢ V = Vtx (G)$
2	1	clnbgrvtxel	$⊢ N \in V \to N \in (G ClNeighbVtx N)$
3		ne0i	$⊢ N \in (G ClNeighbVtx N) \to G ClNeighbVtx N \neq \emptyset$
4	2 3	syl	$⊢ N \in V \to G ClNeighbVtx N \neq \emptyset$