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 ) ≃𝑙𝑔𝑟 ( 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 2nn ⊢ 2 ∈ ℕ
15 3nn ⊢ 3 ∈ ℕ
16 2lt3 ⊢ 2 < 3
17 elfzo1 ⊢ ( 2 ∈ ( 1 ..^ 3 ) ↔ ( 2 ∈ ℕ ∧ 3 ∈ ℕ ∧ 2 < 3 ) )
18 14 15 16 17 mpbir3an ⊢ 2 ∈ ( 1 ..^ 3 )
19 18 10 eleqtri ⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
20 gpgusgra ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 2 ) ∈ USGraph )
21 1 19 20 mp2an ⊢ ( 5 gPetersenGr 2 ) ∈ USGraph
22 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
23 eluzfz1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 2 ) )
24 22 23 ax-mp ⊢ 1 ∈ ( 1 ... 2 )
25 gpg5order ⊢ ( 1 ∈ ( 1 ... 2 ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = 1 0 )
26 24 25 ax-mp ⊢ ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = 1 0
27 eluzfz2 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 2 ∈ ( 1 ... 2 ) )
28 22 27 ax-mp ⊢ 2 ∈ ( 1 ... 2 )
29 gpg5order ⊢ ( 2 ∈ ( 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 ) ) ∈ V
33 10nn0 ⊢ 1 0 ∈ ℕ0
34 hashvnfin ⊢ ( ( ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ V ∧ 1 0 ∈ ℕ0 ) → ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = 1 0 → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ Fin ) )
35 32 33 34 mp2an ⊢ ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = 1 0 → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ Fin )
36 fvex ⊢ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ V
37 hashvnfin ⊢ ( ( ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ V ∧ 1 0 ∈ ℕ0 ) → ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = 1 0 → ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ Fin ) )
38 36 33 37 mp2an ⊢ ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = 1 0 → ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ Fin )
39 hashen ⊢ ( ( ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ Fin ∧ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ 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 ) ∈ USGraph ∧ ( 5 gPetersenGr 2 ) ∈ USGraph ∧ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) )
44 eqid ⊢ ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 )
45 44 gpg5gricstgr3 ⊢ ( ( 1 ∈ ( 1 ... 2 ) ∧ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) → ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
46 24 45 mpan ⊢ ( 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) → ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
47 46 rgen ⊢ ∀ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 )
48 eqid ⊢ ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
49 48 gpg5gricstgr3 ⊢ ( ( 2 ∈ ( 1 ... 2 ) ∧ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) → ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
50 28 49 mpan ⊢ ( 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) → ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
51 50 rgen ⊢ ∀ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 )
52 3nn0 ⊢ 3 ∈ ℕ0
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 ) ∈ USGraph ∧ ( 5 gPetersenGr 2 ) ∈ USGraph ∧ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( 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 ) ) → ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 ) )
56 43 47 51 55 mp3an ⊢ ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 )