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	|- G = ( StarGr ` N )
	stgrvtx0.v	|- V = ( Vtx ` G )
Assertion	stgrclnbgr0	|- ( N e. NN0 -> ( G ClNeighbVtx 0 ) = V )

Proof

Step	Hyp	Ref	Expression
1		stgrvtx0.g	|- G = ( StarGr ` N )
2		stgrvtx0.v	|- V = ( Vtx ` G )
3	1 2	stgrvtx0	|- ( N e. NN0 -> 0 e. V )
4	2	dfclnbgr4	|- ( 0 e. V -> ( G ClNeighbVtx 0 ) = ( { 0 } u. ( G NeighbVtx 0 ) ) )
5	3 4	syl	|- ( N e. NN0 -> ( G ClNeighbVtx 0 ) = ( { 0 } u. ( G NeighbVtx 0 ) ) )
6	1 2	stgrnbgr0	|- ( N e. NN0 -> ( G NeighbVtx 0 ) = ( V \ { 0 } ) )
7	6	uneq2d	|- ( N e. NN0 -> ( { 0 } u. ( G NeighbVtx 0 ) ) = ( { 0 } u. ( V \ { 0 } ) ) )
8	3	snssd	|- ( N e. NN0 -> { 0 } C_ V )
9		undif	|- ( { 0 } C_ V <-> ( { 0 } u. ( V \ { 0 } ) ) = V )
10	8 9	sylib	|- ( N e. NN0 -> ( { 0 } u. ( V \ { 0 } ) ) = V )
11	5 7 10	3eqtrd	|- ( N e. NN0 -> ( G ClNeighbVtx 0 ) = V )