Theorem stgrclnbgr0

Description: All vertices of a star graph S_N are in the closed neighborhood of the center. (Contributed by AV, 12-Sep-2025)

	Ref	Expression
Hypotheses	stgrvtx0.g	No typesetting found for |- G = ( StarGr ` N ) with typecode |-
	stgrvtx0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	stgrclnbgr0	$$⊢N\in {\mathbb{N}}_0\to GClNeighbVtx0=V$$

Proof

Step	Hyp	Ref	Expression
1		stgrvtx0.g	Could not format G = ( StarGr ` N ) : No typesetting found for |- G = ( StarGr ` N ) with typecode |-
2		stgrvtx0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
3	1 2	stgrvtx0	$$⊢N\in {\mathbb{N}}_0\to 0\in V$$
4	2	dfclnbgr4	$$⊢0\in V\to GClNeighbVtx0=\left\{0\right\}\cup \left(G\mathrm{NeighbVtx}0\right)$$
5	3 4	syl	$$⊢N\in {\mathbb{N}}_0\to GClNeighbVtx0=\left\{0\right\}\cup \left(G\mathrm{NeighbVtx}0\right)$$
6	1 2	stgrnbgr0	$$⊢N\in {\mathbb{N}}_0\to G\mathrm{NeighbVtx}0=V\setminus \left\{0\right\}$$
7	6	uneq2d	$$⊢N\in {\mathbb{N}}_0\to \left\{0\right\}\cup \left(G\mathrm{NeighbVtx}0\right)=\left\{0\right\}\cup \left(V\setminus \left\{0\right\}\right)$$
8	3	snssd	$$⊢N\in {\mathbb{N}}_0\to \left\{0\right\}\subseteq V$$
9		undif	$$⊢\left\{0\right\}\subseteq V\leftrightarrow \left\{0\right\}\cup \left(V\setminus \left\{0\right\}\right)=V$$
10	8 9	sylib	$$⊢N\in {\mathbb{N}}_0\to \left\{0\right\}\cup \left(V\setminus \left\{0\right\}\right)=V$$
11	5 7 10	3eqtrd	$$⊢N\in {\mathbb{N}}_0\to GClNeighbVtx0=V$$