Metamath Proof Explorer

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 
|- ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 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 pgjsgr 
 |-  ( 5 gPetersenGr 2 ) e. USGraph
15 f1oi 
 |-  ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( { 0 , 1 } X. ( 0 ..^ 5 ) ) -1-1-onto-> ( { 0 , 1 } X. ( 0 ..^ 5 ) )
16 5nn 
 |-  5 e. NN
17 pglem 
 |-  2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
18 eqidd 
 |-  ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) = ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) )
19 11 a1i 
 |-  ( 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) -> 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) )
20 eqid 
 |-  ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) = ( 1 ..^ ( |^ ` ( 5 / 2 ) ) )
21 eqid 
 |-  ( 0 ..^ 5 ) = ( 0 ..^ 5 )
22 20 21 gpgvtx 
 |-  ( ( 5 e. NN /\ 1 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) )
23 19 22 sylan2 
 |-  ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) )
24 20 21 gpgvtx 
 |-  ( ( 5 e. NN /\ 2 e. ( 1 ..^ ( |^ ` ( 5 / 2 ) ) ) ) -> ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( { 0 , 1 } X. ( 0 ..^ 5 ) ) )
25 18 23 24 f1oeq123d 
 |-  ( ( 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 ) ) ) )
26 16 17 25 mp2an 
 |-  ( ( _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 ) ) )
27 15 26 mpbir 
 |-  ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) : ( Vtx ` ( 5 gPetersenGr 1 ) ) -1-1-onto-> ( Vtx ` ( 5 gPetersenGr 2 ) )
28 13 14 27 3pm3.2i 
 |-  ( ( 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 ) ) )
29 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
30 eluzfz1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... 2 ) )
31 29 30 ax-mp 
 |-  1 e. ( 1 ... 2 )
32 eqid 
 |-  ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 )
33 32 gpg5gricstgr3 
 |-  ( ( 1 e. ( 1 ... 2 ) /\ v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) )
34 31 33 mpan 
 |-  ( v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) -> ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 ) )
35 34 rgen 
 |-  A. v e. ( Vtx ` ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx v ) ) ~=gr ( StarGr ` 3 )
36 eluzfz2 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> 2 e. ( 1 ... 2 ) )
37 29 36 ax-mp 
 |-  2 e. ( 1 ... 2 )
38 eqid 
 |-  ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
39 38 gpg5gricstgr3 
 |-  ( ( 2 e. ( 1 ... 2 ) /\ w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) )
40 37 39 mpan 
 |-  ( w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) -> ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 ) )
41 40 rgen 
 |-  A. w e. ( Vtx ` ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx w ) ) ~=gr ( StarGr ` 3 )
42 3nn0 
 |-  3 e. NN0
43 eqid 
 |-  ( Vtx ` ( 5 gPetersenGr 1 ) ) = ( Vtx ` ( 5 gPetersenGr 1 ) )
44 eqid 
 |-  ( Vtx ` ( 5 gPetersenGr 2 ) ) = ( Vtx ` ( 5 gPetersenGr 2 ) )
45 42 43 44 clnbgr3stgrgrlim 
 |-  ( ( ( ( 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 ) ) )
46 28 35 41 45 mp3an 
 |-  ( _I |` ( { 0 , 1 } X. ( 0 ..^ 5 ) ) ) e. ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) )