Theorem opgpgvtx

Description: A vertex in a generalized Petersen graph G as ordered pair. (Contributed by AV, 1-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		opgpgvtx.i	$$⊢I=\left(0..^N\right)$$
2		opgpgvtx.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
3		opgpgvtx.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
4		opgpgvtx.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		eluz3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
8	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 |-
9	7 8	sylan	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) ) with typecode |-
10	6 9	eqtrid	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to V=\left\{0,1\right\}\times I$$
11	10	eleq2d	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(⟨X,Y⟩\in V\leftrightarrow ⟨X,Y⟩\in \left(\left\{0,1\right\}\times I\right)\right)$$
12		opelxp	$$⊢⟨X,Y⟩\in \left(\left\{0,1\right\}\times I\right)\leftrightarrow \left(X\in \left\{0,1\right\}\wedge Y\in I\right)$$
13	12	a1i	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(⟨X,Y⟩\in \left(\left\{0,1\right\}\times I\right)\leftrightarrow \left(X\in \left\{0,1\right\}\wedge Y\in I\right)\right)$$
14		c0ex	$$⊢0\in \mathrm{V}$$
15		1ex	$$⊢1\in \mathrm{V}$$
16	14 15	elpr2	$$⊢X\in \left\{0,1\right\}\leftrightarrow \left(X=0\vee X=1\right)$$
17	16	a1i	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(X\in \left\{0,1\right\}\leftrightarrow \left(X=0\vee X=1\right)\right)$$
18	17	anbi1d	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(\left(X\in \left\{0,1\right\}\wedge Y\in I\right)\leftrightarrow \left(\left(X=0\vee X=1\right)\wedge Y\in I\right)\right)$$
19	11 13 18	3bitrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in J\right)\to \left(⟨X,Y⟩\in V\leftrightarrow \left(\left(X=0\vee X=1\right)\wedge Y\in I\right)\right)$$