Metamath Proof Explorer


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 = Vtx G
Assertion stgrclnbgr0 N 0 G ClNeighbVtx 0 = 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 = Vtx G
3 1 2 stgrvtx0 N 0 0 V
4 2 dfclnbgr4 0 V G ClNeighbVtx 0 = 0 G NeighbVtx 0
5 3 4 syl N 0 G ClNeighbVtx 0 = 0 G NeighbVtx 0
6 1 2 stgrnbgr0 N 0 G NeighbVtx 0 = V 0
7 6 uneq2d N 0 0 G NeighbVtx 0 = 0 V 0
8 3 snssd N 0 0 V
9 undif 0 V 0 V 0 = V
10 8 9 sylib N 0 0 V 0 = V
11 5 7 10 3eqtrd N 0 G ClNeighbVtx 0 = V