Theorem gpgvtxel2

Description: The second component of a vertex in a generalized Petersen graph G . (Contributed by AV, 30-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	gpgvtxel2	$$⊢\left(\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\wedge X\in V\right)\to 2^{nd}\left(X\right)\in I$$

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	1 2 3 4	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)$$
6		simpr	$$⊢\left(x\in \left\{0,1\right\}\wedge y\in I\right)\to y\in I$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	op2ndd	$$⊢X=⟨x,y⟩\to 2^{nd}\left(X\right)=y$$
10	9	eleq1d	$$⊢X=⟨x,y⟩\to \left(2^{nd}\left(X\right)\in I\leftrightarrow y\in I\right)$$
11	6 10	syl5ibrcom	$$⊢\left(x\in \left\{0,1\right\}\wedge y\in I\right)\to \left(X=⟨x,y⟩\to 2^{nd}\left(X\right)\in I\right)$$
12	11	rexlimivv	$$⊢\exists x\in \left\{0,1\right\}\exists y\in IX=⟨x,y⟩\to 2^{nd}\left(X\right)\in I$$
13	5 12	biimtrdi	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(X\in V\to 2^{nd}\left(X\right)\in I\right)$$
14	13	imp	$$⊢\left(\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\wedge X\in V\right)\to 2^{nd}\left(X\right)\in I$$