Theorem gpgvtxel

Description: A vertex in a generalized Petersen graph G . (Contributed by AV, 29-Aug-2025)

	Ref	Expression
Hypotheses	gpgvtxel.i	$$⊢I=\left(0..^N\right)$$
	gpgvtxel.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
	gpgvtxel.g	No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
	gpgvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	gpgvtxel	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(X\in V\leftrightarrow \exists x\in \left\{0,1\right\}\exists y\in IX=⟨x,y⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		gpgvtxel.i	$$⊢I=\left(0..^N\right)$$
2		gpgvtxel.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
3		gpgvtxel.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
4		gpgvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
5	3	fveq2i	Could not format ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for |- ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) with typecode |-
6	4 5	eqtri	Could not format V = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for |- V = ( Vtx ` ( N gPetersenGr K ) ) with typecode |-
7	6	eleq2i	Could not format ( X e. V <-> X e. ( Vtx ` ( N gPetersenGr K ) ) ) : No typesetting found for |- ( X e. V <-> X e. ( Vtx ` ( N gPetersenGr K ) ) ) with typecode |-
8		eluzge3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
9	2 1	gpgvtx	Could not format ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) ) with typecode |-
10	9	eleq2d	Could not format ( ( N e. NN /\ K e. J ) -> ( X e. ( Vtx ` ( N gPetersenGr K ) ) <-> X e. ( { 0 , 1 } X. I ) ) ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( X e. ( Vtx ` ( N gPetersenGr K ) ) <-> X e. ( { 0 , 1 } X. I ) ) ) with typecode |-
11	8 10	sylan	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. ( Vtx ` ( N gPetersenGr K ) ) <-> X e. ( { 0 , 1 } X. I ) ) ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. ( Vtx ` ( N gPetersenGr K ) ) <-> X e. ( { 0 , 1 } X. I ) ) ) with typecode |-
12	7 11	bitrid	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(X\in V\leftrightarrow X\in \left(\left\{0,1\right\}\times I\right)\right)$$
13		elxp2	$$⊢X\in \left(\left\{0,1\right\}\times I\right)\leftrightarrow \exists x\in \left\{0,1\right\}\exists y\in IX=⟨x,y⟩$$
14	12 13	bitrdi	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(X\in V\leftrightarrow \exists x\in \left\{0,1\right\}\exists y\in IX=⟨x,y⟩\right)$$