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	⊢ 𝐺 = ( StarGr ‘ 𝑁 )
	stgrvtx0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	stgrclnbgr0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐺 ClNeighbVtx 0 ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		stgrvtx0.g	⊢ 𝐺 = ( StarGr ‘ 𝑁 )
2		stgrvtx0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3	1 2	stgrvtx0	⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ 𝑉 )
4	2	dfclnbgr4	⊢ ( 0 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 0 ) = ( { 0 } ∪ ( 𝐺 NeighbVtx 0 ) ) )
5	3 4	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐺 ClNeighbVtx 0 ) = ( { 0 } ∪ ( 𝐺 NeighbVtx 0 ) ) )
6	1 2	stgrnbgr0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐺 NeighbVtx 0 ) = ( 𝑉 ∖ { 0 } ) )
7	6	uneq2d	⊢ ( 𝑁 ∈ ℕ0 → ( { 0 } ∪ ( 𝐺 NeighbVtx 0 ) ) = ( { 0 } ∪ ( 𝑉 ∖ { 0 } ) ) )
8	3	snssd	⊢ ( 𝑁 ∈ ℕ0 → { 0 } ⊆ 𝑉 )
9		undif	⊢ ( { 0 } ⊆ 𝑉 ↔ ( { 0 } ∪ ( 𝑉 ∖ { 0 } ) ) = 𝑉 )
10	8 9	sylib	⊢ ( 𝑁 ∈ ℕ0 → ( { 0 } ∪ ( 𝑉 ∖ { 0 } ) ) = 𝑉 )
11	5 7 10	3eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐺 ClNeighbVtx 0 ) = 𝑉 )