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 } × ( 0 ..^ 5 ) ) ) ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) )

Proof

Step Hyp Ref Expression
1 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
2 3z ⊢ 3 ∈ ℤ
3 1lt3 ⊢ 1 < 3
4 eluz2b1 ⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 3 ∈ ℤ ∧ 1 < 3 ) )
5 2 3 4 mpbir2an ⊢ 3 ∈ ( ℤ≥ ‘ 2 )
6 fzo1lb ⊢ ( 1 ∈ ( 1 ..^ 3 ) ↔ 3 ∈ ( ℤ≥ ‘ 2 ) )
7 5 6 mpbir ⊢ 1 ∈ ( 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 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
12 gpgusgra ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 1 ) ∈ USGraph )
13 1 11 12 mp2an ⊢ ( 5 gPetersenGr 1 ) ∈ USGraph
14 pgjsgr ⊢ ( 5 gPetersenGr 2 ) ∈ USGraph
15 f1oi ⊢ ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) : ( { 0 , 1 } × ( 0 ..^ 5 ) ) –1-1-onto→ ( { 0 , 1 } × ( 0 ..^ 5 ) )
16 5nn ⊢ 5 ∈ ℕ
17 pglem ⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
18 eqidd ⊢ ( ( 5 ∈ ℕ ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) = ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) )
19 11 a1i ⊢ ( 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
20 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
21 eqid ⊢ ( 0 ..^ 5 ) = ( 0 ..^ 5 )
22 20 21 gpgvtx ⊢ ( ( 5 ∈ ℕ ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 5 ) ) )
23 19 22 sylan2 ⊢ ( ( 5 ∈ ℕ ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) = ( { 0 , 1 } × ( 0 ..^ 5 ) ) )
24 20 21 gpgvtx ⊢ ( ( 5 ∈ ℕ ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( Vtx ‘ ( 5 gPetersenGr 2 ) ) = ( { 0 , 1 } × ( 0 ..^ 5 ) ) )
25 18 23 24 f1oeq123d ⊢ ( ( 5 ∈ ℕ ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) : ( Vtx ‘ ( 5 gPetersenGr 1 ) ) –1-1-onto→ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ↔ ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) : ( { 0 , 1 } × ( 0 ..^ 5 ) ) –1-1-onto→ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) )
26 16 17 25 mp2an ⊢ ( ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) : ( Vtx ‘ ( 5 gPetersenGr 1 ) ) –1-1-onto→ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ↔ ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) : ( { 0 , 1 } × ( 0 ..^ 5 ) ) –1-1-onto→ ( { 0 , 1 } × ( 0 ..^ 5 ) ) )
27 15 26 mpbir ⊢ ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) : ( Vtx ‘ ( 5 gPetersenGr 1 ) ) –1-1-onto→ ( Vtx ‘ ( 5 gPetersenGr 2 ) )
28 13 14 27 3pm3.2i ⊢ ( ( 5 gPetersenGr 1 ) ∈ USGraph ∧ ( 5 gPetersenGr 2 ) ∈ USGraph ∧ ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) : ( Vtx ‘ ( 5 gPetersenGr 1 ) ) –1-1-onto→ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) )
29 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
30 eluzfz1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 2 ) )
31 29 30 ax-mp ⊢ 1 ∈ ( 1 ... 2 )
32 eqid ⊢ ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 )
33 32 gpg5gricstgr3 ⊢ ( ( 1 ∈ ( 1 ... 2 ) ∧ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) → ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
34 31 33 mpan ⊢ ( 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) → ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
35 34 rgen ⊢ ∀ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 )
36 eluzfz2 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 2 ∈ ( 1 ... 2 ) )
37 29 36 ax-mp ⊢ 2 ∈ ( 1 ... 2 )
38 eqid ⊢ ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
39 38 gpg5gricstgr3 ⊢ ( ( 2 ∈ ( 1 ... 2 ) ∧ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) → ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
40 37 39 mpan ⊢ ( 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) → ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
41 40 rgen ⊢ ∀ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 )
42 3nn0 ⊢ 3 ∈ ℕ0
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 ) ∈ USGraph ∧ ( 5 gPetersenGr 2 ) ∈ USGraph ∧ ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) : ( Vtx ‘ ( 5 gPetersenGr 1 ) ) –1-1-onto→ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) ) → ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) ) )
46 28 35 41 45 mp3an ⊢ ( I ↾ ( { 0 , 1 } × ( 0 ..^ 5 ) ) ) ∈ ( ( 5 gPetersenGr 1 ) GraphLocIso ( 5 gPetersenGr 2 ) )