Theorem stgrvtx0

Description: The center ("internal node") 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	stgrvtx0	$$⊢N\in {\mathbb{N}}_0\to 0\in 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=\mathrm{Vtx}\left(G\right)$$
3		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 |-
4	1	fveq2i	Could not format ( Vtx ` G ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` G ) = ( Vtx ` ( StarGr ` N ) ) with typecode |-
5	2 4	eqtri	Could not format V = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- V = ( Vtx ` ( StarGr ` N ) ) with typecode |-
6	5	eqeq1i	Could not format ( V = ( 0 ... N ) <-> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) : No typesetting found for |- ( V = ( 0 ... N ) <-> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) with typecode |-
7		0elfz	$$⊢N\in {\mathbb{N}}_0\to 0\in \left(0\dots N\right)$$
8		eleq2	$$⊢V=\left(0\dots N\right)\to \left(0\in V\leftrightarrow 0\in \left(0\dots N\right)\right)$$
9	7 8	syl5ibrcom	$$⊢N\in {\mathbb{N}}_0\to \left(V=\left(0\dots N\right)\to 0\in V\right)$$
10	6 9	biimtrrid	Could not format ( N e. NN0 -> ( ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) -> 0 e. V ) ) : No typesetting found for |- ( N e. NN0 -> ( ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) -> 0 e. V ) ) with typecode |-
11	3 10	mpd	$$⊢N\in {\mathbb{N}}_0\to 0\in V$$