Metamath Proof Explorer


Theorem stgrorder

Description: The order of a star graph S_N. (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 stgrorder N 0 V = N + 1

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 fveq2i Could not format ( Vtx ` G ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` G ) = ( Vtx ` ( StarGr ` N ) ) with typecode |-
4 2 3 eqtri Could not format V = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- V = ( Vtx ` ( StarGr ` N ) ) with typecode |-
5 stgrvtx Could not format ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) : No typesetting found for |- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) with typecode |-
6 4 5 eqtrid N 0 V = 0 N
7 6 fveq2d N 0 V = 0 N
8 hashfz0 N 0 0 N = N + 1
9 7 8 eqtrd N 0 V = N + 1