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)

	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		2nn	$$⊢2\in \mathbb{N}$$
15		3nn	$$⊢3\in \mathbb{N}$$
16		2lt3	$$⊢2<3$$
17		elfzo1	$$⊢2\in \left(1..^3\right)\leftrightarrow \left(2\in \mathbb{N}\wedge 3\in \mathbb{N}\wedge 2<3\right)$$
18	14 15 16 17	mpbir3an	$$⊢2\in \left(1..^3\right)$$
19	18 10	eleqtri	$$⊢2\in \left(1..^⌈\frac{5}{2}⌉\right)$$
20		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 |-
21	1 19 20	mp2an	Could not format ( 5 gPetersenGr 2 ) e. USGraph : No typesetting found for |- ( 5 gPetersenGr 2 ) e. USGraph with typecode |-
22		2eluzge1	$$⊢2\in {\mathbb{Z}}_{\ge 1}$$
23		eluzfz1	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots 2\right)$$
24	22 23	ax-mp	$$⊢1\in \left(1\dots 2\right)$$
25		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 |-
26	24 25	ax-mp	Could not format ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 : No typesetting found for |- ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 with typecode |-
27		eluzfz2	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to 2\in \left(1\dots 2\right)$$
28	22 27	ax-mp	$$⊢2\in \left(1\dots 2\right)$$
29		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 |-
30	28 29	ax-mp	Could not format ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 : No typesetting found for |- ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 with typecode |-
31		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 |-
32		fvex	Could not format ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V with typecode |-
33		10nn0	$$⊢10\in {\mathbb{N}}_0$$
34		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 |-
35	32 33 34	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 |-
36		fvex	Could not format ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V : No typesetting found for |- ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V with typecode |-
37		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 |-
38	36 33 37	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 |-
39		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 |-
40	35 38 39	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 |-
41	31 40	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 |-
42	26 30 41	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 |-
43	13 21 42	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 |-
44		eqid	Could not format ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) : No typesetting found for |- ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 ) with typecode |-
45	44	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 |-
46	24 45	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 |-
47	46	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 |-
48		eqid	Could not format ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) : No typesetting found for |- ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 ) with typecode |-
49	48	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 |-
50	28 49	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 |-
51	50	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 |-
52		3nn0	$$⊢3\in {\mathbb{N}}_0$$
53		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 |-
54		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 |-
55	52 53 54	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 |-
56	43 47 51 55	mp3an	Could not format ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) : No typesetting found for |- ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) with typecode |-