Metamath Proof Explorer

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 
|- ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 )

Proof

Step Hyp Ref Expression
1 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
2 3z 
 |-  3 e. ZZ
3 1lt3 
 |-  1 < 3
4 eluz2b1 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 3 e. ZZ /\ 1 < 3 ) )
5 2 3 4 mpbir2an 
 |-  3 e. ( ZZ>= ` 2 )
6 fzo1lb 
 |-  ( 1 e. ( 1 ..^ 3 ) <-> 3 e. ( ZZ>= ` 2 ) )
7 5 6 mpbir 
 |-  1 e. ( 1 ..^ 3 )
8 ceil5half3 
 |-  ( |^ ` ( 5 / 2 ) ) = 3
9 8 eqcomi 
 |-  3 = ( |^ ` ( 5 / 2 ) )
10 9 oveq2i 
 |-  ( 1 ..^ 3 ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
11 7 10 eleqtri 
 |-  1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
12 gpgusgra 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 1 ) e. USGraph )
13 1 11 12 mp2an 
 |-  ( 5 gPetersenGr 1 ) e. USGraph
14 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
15 gpgusgra 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph )
16 1 14 15 mp2an 
 |-  ( 5 gPetersenGr 2 ) e. USGraph
17 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
18 eluzfz1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... 2 ) )
19 17 18 ax-mp 
 |-  1 e. ( 1 ... 2 )
20 gpg5order 
 |-  ( 1 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 )
21 19 20 ax-mp 
 |-  ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0
22 eluzfz2 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> 2 e. ( 1 ... 2 ) )
23 17 22 ax-mp 
 |-  2 e. ( 1 ... 2 )
24 gpg5order 
 |-  ( 2 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 )
25 23 24 ax-mp 
 |-  ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0
26 eqtr3 
 |-  ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) )
27 fvex 
 |-  ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V
28 10nn0 
 |-  ; 1 0 e. NN0
29 hashvnfin 
 |-  ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) )
30 27 28 29 mp2an 
 |-  ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin )
31 fvex 
 |-  ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V
32 hashvnfin 
 |-  ( ( ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) )
33 31 28 32 mp2an 
 |-  ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin )
34 hashen 
 |-  ( ( ( 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 ) ) ) )
35 30 33 34 syl2an 
 |-  ( ( ( # ` ( 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 ) ) ) )
36 26 35 mpbid 
 |-  ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) )
37 21 25 36 mp2an 
 |-  ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) )
38 13 16 37 3pm3.2i 
 |-  ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) )
39 eqid 
 |-  ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 )
40 39 gpg5gricstgr3 
 |-  ( ( 1 e. ( 1 ... 2 ) /\ v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) )
41 19 40 mpan 
 |-  ( v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) )
42 41 rgen 
 |-  A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 )
43 eqid 
 |-  ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
44 43 gpg5gricstgr3 
 |-  ( ( 2 e. ( 1 ... 2 ) /\ w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) )
45 23 44 mpan 
 |-  ( w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) )
46 45 rgen 
 |-  A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 )
47 3nn0 
 |-  3 e. NN0
48 eqid 
 |-  ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( Vtx ` ( 5 gPetersenGr 1 ) )
49 eqid 
 |-  ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( Vtx ` ( 5 gPetersenGr 2 ) )
50 47 48 49 clnbgr3stgrgrlic 
 |-  ( ( ( ( 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 ) )
51 38 42 46 50 mp3an 
 |-  ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 )