Theorem gpgvtxel

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

	Ref	Expression
Hypotheses	gpgvtxel.i	|- I = ( 0 ..^ N )
	gpgvtxel.j	|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
	gpgvtxel.g	|- G = ( N gPetersenGr K )
	gpgvtxel.v	|- V = ( Vtx ` G )
Assertion	gpgvtxel	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V <-> E. x e. { 0 , 1 } E. y e. I X = <. x , y >. ) )

Proof

Step	Hyp	Ref	Expression
1		gpgvtxel.i	|- I = ( 0 ..^ N )
2		gpgvtxel.j	|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
3		gpgvtxel.g	|- G = ( N gPetersenGr K )
4		gpgvtxel.v	|- V = ( Vtx ` G )
5	3	fveq2i	|- ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) )
6	4 5	eqtri	|- V = ( Vtx ` ( N gPetersenGr K ) )
7	6	eleq2i	|- ( X e. V <-> X e. ( Vtx ` ( N gPetersenGr K ) ) )
8		eluzge3nn	|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )
9	2 1	gpgvtx	|- ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) )
10	9	eleq2d	|- ( ( N e. NN /\ K e. J ) -> ( X e. ( Vtx ` ( N gPetersenGr K ) ) <-> X e. ( { 0 , 1 } X. I ) ) )
11	8 10	sylan	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. ( Vtx ` ( N gPetersenGr K ) ) <-> X e. ( { 0 , 1 } X. I ) ) )
12	7 11	bitrid	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V <-> X e. ( { 0 , 1 } X. I ) ) )
13		elxp2	|- ( X e. ( { 0 , 1 } X. I ) <-> E. x e. { 0 , 1 } E. y e. I X = <. x , y >. )
14	12 13	bitrdi	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( X e. V <-> E. x e. { 0 , 1 } E. y e. I X = <. x , y >. ) )