Theorem gpgiedg

Description: The indexed edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025)

	Ref	Expression
Hypotheses	gpgov.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
	gpgov.i	$$⊢I=\left(0..^N\right)$$
Assertion	gpgiedg	Could not format assertion : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		gpgov.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
2		gpgov.i	$$⊢I=\left(0..^N\right)$$
3	1 2	gpgov	Could not format ( ( N e. NN /\ K e. J ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) with typecode |-
4	3	fveq2d	Could not format ( ( N e. NN /\ K e. J ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) ) with typecode |-
5		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
6	2	ovexi	$$⊢I\in \mathrm{V}$$
7	5 6	xpex	$$⊢\left\{0,1\right\}\times I\in \mathrm{V}$$
8		eqid	$$⊢\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}=\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}$$
9	5	a1i	$$⊢I=\left(0..^N\right)\to \left\{0,1\right\}\in \mathrm{V}$$
10		ovexd	$$⊢I=\left(0..^N\right)\to \left(0..^N\right)\in \mathrm{V}$$
11	2 10	eqeltrid	$$⊢I=\left(0..^N\right)\to I\in \mathrm{V}$$
12	9 11	xpexd	$$⊢I=\left(0..^N\right)\to \left\{0,1\right\}\times I\in \mathrm{V}$$
13	12	pwexd	$$⊢I=\left(0..^N\right)\to 𝒫\left(\left\{0,1\right\}\times I\right)\in \mathrm{V}$$
14	8 13	rabexd	$$⊢I=\left(0..^N\right)\to \left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}\in \mathrm{V}$$
15	14	resiexd	$$⊢I=\left(0..^N\right)\to {\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}\in \mathrm{V}$$
16	2 15	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}\in \mathrm{V}$$
17	7 16	pm3.2i	$$⊢\left(\left\{0,1\right\}\times I\in \mathrm{V}\wedge {\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}\in \mathrm{V}\right)$$
18		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times I⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times I⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}⟩\right\}$$
19	18	struct2griedg	$$⊢\left(\left\{0,1\right\}\times I\in \mathrm{V}\wedge {\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times I⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}⟩\right\}\right)={\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}$$
20	17 19	mp1i	$$⊢\left(N\in \mathbb{N}\wedge K\in J\right)\to \mathrm{iEdg}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times I⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}⟩\right\}\right)={\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times I\right)|\exists x\in I\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}N⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+K\right)\mathrm{mod}N⟩\right\}\right)\right\}}$$
21	4 20	eqtrd	Could not format ( ( N e. NN /\ K e. J ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) ) with typecode |-