Theorem gpg5grlic

Description: 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), are locally isomorphic. (Contributed by AV, 29-Sep-2025) (Proof shortened by AV, 22-Nov-2025)

	Ref	Expression
Assertion	gpg5grlic	Could not format assertion : No typesetting found for |- ( 5 gPetersenGr 1 ) ~=lgr ( 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		pglem	$$⊢2\in \left(1..^⌈\frac{5}{2}⌉\right)$$
15		gpgusgra	Could not format ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph ) : No typesetting found for |- ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph ) with typecode |-
16	1 14 15	mp2an	Could not format ( 5 gPetersenGr 2 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USGraph with typecode |-
17		2eluzge1	$$⊢2\in {\mathbb{Z}}_{\ge 1}$$
18		eluzfz1	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots 2\right)$$
19	17 18	ax-mp	$$⊢1\in \left(1\dots 2\right)$$
20		gpg5order	Could not format ( 1 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 ) : No typesetting found for |- ( 1 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 ) with typecode |-
21	19 20	ax-mp	Could not format ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 : No typesetting found for |- ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 with typecode |-
22		eluzfz2	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to 2\in \left(1\dots 2\right)$$
23	17 22	ax-mp	$$⊢2\in \left(1\dots 2\right)$$
24		gpg5order	Could not format ( 2 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) : No typesetting found for |- ( 2 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) with typecode |-
25	23 24	ax-mp	Could not format ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 : No typesetting found for |- ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 with typecode |-
26		eqtr3	Could not format ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
27		fvex	Could not format ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V with typecode |-
28		10nn0	$$⊢10\in {\mathbb{N}}_0$$
29		hashvnfin	Could not format ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) ) : No typesetting found for |- ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) ) with typecode |-
30	27 28 29	mp2an	Could not format ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) : No typesetting found for |- ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) with typecode |-
31		fvex	Could not format ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V with typecode |-
32		hashvnfin	Could not format ( ( ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) ) : No typesetting found for |- ( ( ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) ) with typecode |-
33	31 28 32	mp2an	Could not format ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) : No typesetting found for |- ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) with typecode |-
34		hashen	Could not format ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin /\ ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) <-> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin /\ ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) <-> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
35	30 33 34	syl2an	Could not format ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) <-> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) : No typesetting found for |- ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) <-> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) ) with typecode |-
36	26 35	mpbid	Could not format ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
37	21 25 36	mp2an	Could not format ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) with typecode |-
38	13 16 37	3pm3.2i	Could not format ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) : No typesetting found for |- ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) ) with typecode |-
39		eqid	Could not format ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) : No typesetting found for |- ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) with typecode |-
40	39	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 |-
41	19 40	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 |-
42	41	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 |-
43		eqid	Could not format ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) : No typesetting found for |- ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) with typecode |-
44	43	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 |-
45	23 44	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 |-
46	45	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 |-
47		3nn0	$$⊢3\in {\mathbb{N}}_0$$
48		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 |-
49		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 |-
50	47 48 49	clnbgr3stgrgrlic	Could not format ( ( ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( 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 ) ) -> ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) ) : No typesetting found for |- ( ( ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( 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 ) ) -> ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) ) with typecode |-
51	38 42 46 50	mp3an	Could not format ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) : No typesetting found for |- ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) with typecode |-