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 ) ≃𝑙𝑔𝑟 ( 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 pglem ⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
15 gpgusgra ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 2 ) ∈ USGraph )
16 1 14 15 mp2an ⊢ ( 5 gPetersenGr 2 ) ∈ USGraph
17 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
18 eluzfz1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 2 ) )
19 17 18 ax-mp ⊢ 1 ∈ ( 1 ... 2 )
20 gpg5order ⊢ ( 1 ∈ ( 1 ... 2 ) → ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = 1 0 )
21 19 20 ax-mp ⊢ ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = 1 0
22 eluzfz2 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → 2 ∈ ( 1 ... 2 ) )
23 17 22 ax-mp ⊢ 2 ∈ ( 1 ... 2 )
24 gpg5order ⊢ ( 2 ∈ ( 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 ) ) ∈ V
28 10nn0 ⊢ 1 0 ∈ ℕ0
29 hashvnfin ⊢ ( ( ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ V ∧ 1 0 ∈ ℕ0 ) → ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = 1 0 → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ Fin ) )
30 27 28 29 mp2an ⊢ ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) = 1 0 → ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ∈ Fin )
31 fvex ⊢ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ V
32 hashvnfin ⊢ ( ( ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ V ∧ 1 0 ∈ ℕ0 ) → ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = 1 0 → ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ Fin ) )
33 31 28 32 mp2an ⊢ ( ( ♯ ‘ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) = 1 0 → ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ∈ Fin )
34 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 ) ) ) )
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 ) ∈ USGraph ∧ ( 5 gPetersenGr 2 ) ∈ USGraph ∧ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ≈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) )
39 eqid ⊢ ( 5 gPetersenGr 1 ) = ( 5 gPetersenGr 1 )
40 39 gpg5gricstgr3 ⊢ ( ( 1 ∈ ( 1 ... 2 ) ∧ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ) → ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
41 19 40 mpan ⊢ ( 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) → ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
42 41 rgen ⊢ ∀ 𝑣 ∈ ( Vtx ‘ ( 5 gPetersenGr 1 ) ) ( ( 5 gPetersenGr 1 ) ISubGr ( ( 5 gPetersenGr 1 ) ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 )
43 eqid ⊢ ( 5 gPetersenGr 2 ) = ( 5 gPetersenGr 2 )
44 43 gpg5gricstgr3 ⊢ ( ( 2 ∈ ( 1 ... 2 ) ∧ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ) → ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
45 23 44 mpan ⊢ ( 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) → ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 ) )
46 45 rgen ⊢ ∀ 𝑤 ∈ ( Vtx ‘ ( 5 gPetersenGr 2 ) ) ( ( 5 gPetersenGr 2 ) ISubGr ( ( 5 gPetersenGr 2 ) ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( StarGr ‘ 3 )
47 3nn0 ⊢ 3 ∈ ℕ0
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 ) ∈ 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 ) )
51 38 42 46 50 mp3an ⊢ ( 5 gPetersenGr 1 ) ≃𝑙𝑔𝑟 ( 5 gPetersenGr 2 )