Theorem gpg5grlim

Description: A local isomorphism between the two generalized Petersen graphs G(N,K) of order 10 ( N = 5 ), which are the Petersen graph G(5,2) and the 5-prism G(5,1). (Contributed by AV, 28-Dec-2025)

	Ref	Expression
Assertion	gpg5grlim	Could not format assertion : No typesetting found for |- ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		5eluz3	$$⊢5\in {\mathbb{Z}}_{\ge 3}$$
2		3z	$$⊢3\in \mathbb{Z}$$
3		1lt3	$$⊢1<3$$
4		eluz2b1	$$⊢3\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(3\in \mathbb{Z}\wedge 1<3\right)$$
5	2 3 4	mpbir2an	$$⊢3\in {\mathbb{Z}}_{\ge 2}$$
6		fzo1lb	$$⊢1\in \left(1..^3\right)\leftrightarrow 3\in {\mathbb{Z}}_{\ge 2}$$
7	5 6	mpbir	$$⊢1\in \left(1..^3\right)$$
8		ceil5half3	$$⊢⌈\frac{5}{2}⌉=3$$
9	8	eqcomi	$$⊢3=⌈\frac{5}{2}⌉$$
10	9	oveq2i	$$⊢\left(1..^3\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
11	7 10	eleqtri	$$⊢1\in \left(1..^⌈\frac{5}{2}⌉\right)$$
12		gpgusgra	Could not format ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 1 ) e. USGraph ) : No typesetting found for |- ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 1 ) e. USGraph ) with typecode |-
13	1 11 12	mp2an	Could not format ( 5 gPetersenGr 1 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 1 ) e. USGraph with typecode |-
14		pgjsgr	Could not format ( 5 gPetersenGr 2 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USGraph with typecode |-
15		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}\right):\left\{0,1\right\}\times \left(0..^5\right)\underset{1-1\; onto}{⟶}\left\{0,1\right\}\times \left(0..^5\right)$$
16		5nn	$$⊢5\in \mathbb{N}$$
17		pglem	$$⊢2\in \left(1..^⌈\frac{5}{2}⌉\right)$$
18		eqidd	$$⊢\left(5\in \mathbb{N}\wedge 2\in \left(1..^⌈\frac{5}{2}⌉\right)\right)\to {\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}={\mathrm{I}\upharpoonright }_{\left(\left\{0,1\right\}\times \left(0..^5\right)\right)}$$
19	11	a1i	$$⊢2\in \left(1..^⌈\frac{5}{2}⌉\right)\to 1\in \left(1..^⌈\frac{5}{2}⌉\right)$$
20		eqid	$$⊢\left(1..^⌈\frac{5}{2}⌉\right)=\left(1..^⌈\frac{5}{2}⌉\right)$$
21		eqid	$$⊢\left(0..^5\right)=\left(0..^5\right)$$
22	20 21	gpgvtx	Could not format ( ( 5 e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : No typesetting found for |- ( ( 5 e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) with typecode |-
23	19 22	sylan2	Could not format ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : No typesetting found for |- ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) with typecode |-
24	20 21	gpgvtx	Could not format ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : No typesetting found for |- ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) with typecode |-
25	18 23 24	f1oeq123d	Could not format ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) <-> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( { 0 , 1 } X. ( 0 ..^ 5 ) ) -1-1-onto-> ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ) : No typesetting found for |- ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) <-> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( { 0 , 1 } X. ( 0 ..^ 5 ) ) -1-1-onto-> ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) ) with typecode |-
26	16 17 25	mp2an	Could not format ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) <-> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( { 0 , 1 } X. ( 0 ..^ 5 ) ) -1-1-onto-> ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : No typesetting found for |- ( ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) <-> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( { 0 , 1 } X. ( 0 ..^ 5 ) ) -1-1-onto-> ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) with typecode |-
27	15 26	mpbir	Could not format ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) with typecode |-
28	13 14 27	3pm3.2i	Could not format ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
29		2eluzge1	$$⊢2\in {\mathbb{Z}}_{\ge 1}$$
30		eluzfz1	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots 2\right)$$
31	29 30	ax-mp	$$⊢1\in \left(1\dots 2\right)$$
32		eqid	Could not format ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) : No typesetting found for |- ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) with typecode |-
33	32	gpg5gricstgr3	Could not format ( ( 1 e. ( 1 ... 2 ) /\ v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( ( 1 e. ( 1 ... 2 ) /\ v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) ) with typecode |-
34	31 33	mpan	Could not format ( v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) ) with typecode |-
35	34	rgen	Could not format A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) : No typesetting found for |- A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) with typecode |-
36		eluzfz2	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to 2\in \left(1\dots 2\right)$$
37	29 36	ax-mp	$$⊢2\in \left(1\dots 2\right)$$
38		eqid	Could not format ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) : No typesetting found for |- ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) with typecode |-
39	38	gpg5gricstgr3	Could not format ( ( 2 e. ( 1 ... 2 ) /\ w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( ( 2 e. ( 1 ... 2 ) /\ w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) with typecode |-
40	37 39	mpan	Could not format ( w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) : No typesetting found for |- ( w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) with typecode |-
41	40	rgen	Could not format A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) : No typesetting found for |- A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) with typecode |-
42		3nn0	$$⊢3\in {\mathbb{N}}_0$$
43		eqid	Could not format ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( Vtx ` ( 5 gPetersenGr 1 ) ) : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( Vtx ` ( 5 gPetersenGr 1 ) ) with typecode |-
44		eqid	Could not format ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( Vtx ` ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( Vtx ` ( 5 gPetersenGr 2 ) ) with typecode |-
45	42 43 44	clnbgr3stgrgrlim	Could not format ( ( ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) ) /\ A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) /\ A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) -> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( ( ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) ) ) /\ A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) /\ A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) ) -> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) ) with typecode |-
46	28 35 41 45	mp3an	Could not format ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) with typecode |-