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)

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 2nn 
 |-  2 e. NN
15 3nn 
 |-  3 e. NN
16 2lt3 
 |-  2 < 3
17 elfzo1 
 |-  ( 2 e. ( 1 ..^ 3 ) <-> ( 2 e. NN /\ 3 e. NN /\ 2 < 3 ) )
18 14 15 16 17 mpbir3an 
 |-  2 e. ( 1 ..^ 3 )
19 18 10 eleqtri 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
20 gpgusgra 
 |-  ( ( 5 e. ( ZZ>= ` 3 ) /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( 5 gPetersenGr 2 ) e. USGraph )
21 1 19 20 mp2an 
 |-  ( 5 gPetersenGr 2 ) e. USGraph
22 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
23 eluzfz1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... 2 ) )
24 22 23 ax-mp 
 |-  1 e. ( 1 ... 2 )
25 gpg5order 
 |-  ( 1 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 )
26 24 25 ax-mp 
 |-  ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0
27 eluzfz2 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> 2 e. ( 1 ... 2 ) )
28 22 27 ax-mp 
 |-  2 e. ( 1 ... 2 )
29 gpg5order 
 |-  ( 2 e. ( 1 ... 2 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 )
30 28 29 ax-mp 
 |-  ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0
31 eqtr3 
 |-  ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) )
32 fvex 
 |-  ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V
33 10nn0 
 |-  ; 1 0 e. NN0
34 hashvnfin 
 |-  ( ( ( Vtx ` ( 5 gPetersenGr 1 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin ) )
35 32 33 34 mp2an 
 |-  ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 1 ) ) e. Fin )
36 fvex 
 |-  ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V
37 hashvnfin 
 |-  ( ( ( Vtx ` ( 5 gPetersenGr 2 ) ) e. _V /\ ; 1 0 e. NN0 ) -> ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin ) )
38 36 33 37 mp2an 
 |-  ( ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 -> ( Vtx ` ( 5 gPetersenGr 2 ) ) e. Fin )
39 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 ) ) ) )
40 35 38 39 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 ) ) ) )
41 31 40 mpbid 
 |-  ( ( ( # ` ( Vtx ` ( 5 gPetersenGr 1 ) ) ) = ; 1 0 /\ ( # ` ( Vtx ` ( 5 gPetersenGr 2 ) ) ) = ; 1 0 ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) )
42 26 30 41 mp2an 
 |-  ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) )
43 13 21 42 3pm3.2i 
 |-  ( ( 5 gPetersenGr 1 ) e. USGraph /\ ( 5 gPetersenGr 2 ) e. USGraph /\ ( Vtx ` ( 5 gPetersenGr 1 ) ) ~~ ( Vtx ` ( 5 gPetersenGr 2 ) ) )
44 eqid 
 |-  ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 )
45 44 gpg5gricstgr3 
 |-  ( ( 1 e. ( 1 ... 2 ) /\ v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) )
46 24 45 mpan 
 |-  ( v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) )
47 46 rgen 
 |-  A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 )
48 eqid 
 |-  ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
49 48 gpg5gricstgr3 
 |-  ( ( 2 e. ( 1 ... 2 ) /\ w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) )
50 28 49 mpan 
 |-  ( w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) )
51 50 rgen 
 |-  A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 )
52 3nn0 
 |-  3 e. NN0
53 eqid 
 |-  ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( Vtx ` ( 5 gPetersenGr 1 ) )
54 eqid 
 |-  ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( Vtx ` ( 5 gPetersenGr 2 ) )
55 52 53 54 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 ) )
56 43 47 51 55 mp3an 
 |-  ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 )