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=\mathrm{Vtx}\left(G\right)$$
Assertion	stgrorder	$$⊢N\in {\mathbb{N}}_0\to \left|V\right|=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=\mathrm{Vtx}\left(G\right)$$
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\in {\mathbb{N}}_0\to V=\left(0\dots N\right)$$
7	6	fveq2d	$$⊢N\in {\mathbb{N}}_0\to \left|V\right|=\left|\left(0\dots N\right)\right|$$
8		hashfz0	$$⊢N\in {\mathbb{N}}_0\to \left|\left(0\dots N\right)\right|=N+1$$
9	7 8	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \left|V\right|=N+1$$