Theorem gpgusgra

Description: The generalized Petersen graph GPG(N,K) is a simple graph. (Contributed by AV, 27-Aug-2025)

	Ref	Expression
Assertion	gpgusgra	Could not format assertion : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\underset{1-1\; onto}{⟶}\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}$$
2		f1of1	$$⊢\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\underset{1-1\; onto}{⟶}\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\to \left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\underset{1-1}{⟶}\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}$$
3	1 2	mp1i	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in \left(1..^⌈\frac{N}{2}⌉\right)\right)\to \left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\underset{1-1}{⟶}\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}$$
4		eqid	$$⊢\left(1..^⌈\frac{N}{2}⌉\right)=\left(1..^⌈\frac{N}{2}⌉\right)$$
5		eqid	$$⊢\left(0..^N\right)=\left(0..^N\right)$$
6	4 5	gpgusgralem	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in \left(1..^⌈\frac{N}{2}⌉\right)\right)\to \left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\subseteq \left\{p\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\left|p\right|=2\right\}$$
7		f1ss	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\underset{1-1}{⟶}\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\wedge \left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\subseteq \left\{p\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\left|p\right|=2\right\}\right)\to \left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\underset{1-1}{⟶}\left\{p\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\left|p\right|=2\right\}$$
8	3 6 7	syl2anc	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in \left(1..^⌈\frac{N}{2}⌉\right)\right)\to \left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}\underset{1-1}{⟶}\left\{p\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\left|p\right|=2\right\}$$
9		eluzge3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
10	4 5	gpgiedg	Could not format ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( 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. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) ) with typecode |-
11	9 10	sylan	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( 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. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr K ) ) = ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) ) with typecode |-
12	11	dmeqd	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> dom ( iEdg ` ( N gPetersenGr K ) ) = dom ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( 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. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> dom ( iEdg ` ( N gPetersenGr K ) ) = dom ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) ) with typecode |-
13		dmresi	$$⊢\mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^N\right)\right)|\exists x\in \left(0..^N\right)\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\}$$
14	12 13	eqtrdi	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> dom ( iEdg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( 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. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> dom ( iEdg ` ( N gPetersenGr K ) ) = { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) with typecode |-
15	4 5	gpgvtx	Could not format ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for |- ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode |-
16	9 15	sylan	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode |-
17	16	pweqd	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ~P ( Vtx ` ( N gPetersenGr K ) ) = ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ~P ( Vtx ` ( N gPetersenGr K ) ) = ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) with typecode |-
18	17	rabeqdv	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } = { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } = { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } ) with typecode |-
19	11 14 18	f1eq123d	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } <-> ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) : { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } -1-1-> { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } ) ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } <-> ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) : { e e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | E. x e. ( 0 ..^ N ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } -1-1-> { p e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) | ( # ` p ) = 2 } ) ) with typecode |-
20	8 19	mpbird	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } ) with typecode |-
21		ovex	Could not format ( N gPetersenGr K ) e. _V : No typesetting found for |- ( N gPetersenGr K ) e. _V with typecode |-
22		eqid	Could not format ( Vtx ` ( N gPetersenGr K ) ) = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for |- ( Vtx ` ( N gPetersenGr K ) ) = ( Vtx ` ( N gPetersenGr K ) ) with typecode |-
23		eqid	Could not format ( iEdg ` ( N gPetersenGr K ) ) = ( iEdg ` ( N gPetersenGr K ) ) : No typesetting found for |- ( iEdg ` ( N gPetersenGr K ) ) = ( iEdg ` ( N gPetersenGr K ) ) with typecode |-
24	22 23	isusgrs	Could not format ( ( N gPetersenGr K ) e. _V -> ( ( N gPetersenGr K ) e. USGraph <-> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } ) ) : No typesetting found for |- ( ( N gPetersenGr K ) e. _V -> ( ( N gPetersenGr K ) e. USGraph <-> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } ) ) with typecode |-
25	21 24	mp1i	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( ( N gPetersenGr K ) e. USGraph <-> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } ) ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( ( N gPetersenGr K ) e. USGraph <-> ( iEdg ` ( N gPetersenGr K ) ) : dom ( iEdg ` ( N gPetersenGr K ) ) -1-1-> { p e. ~P ( Vtx ` ( N gPetersenGr K ) ) | ( # ` p ) = 2 } ) ) with typecode |-
26	20 25	mpbird	Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph ) with typecode |-