Theorem gpg5ngric

Description: The two generalized Petersen graphs G(5,K) of order 10, which are the Petersen graph G(5,2) and the 5-prism G(5,1), are not isomorphic. (Contributed by AV, 22-Nov-2025)

	Ref	Expression
Assertion	gpg5ngric	⊢ ¬ ( 5 gPetersenGr 1 ) ≃𝑔𝑟 ( 5 gPetersenGr 2 )

Proof

Step	Hyp	Ref	Expression
1		5eluz3	⊢ 5 ∈ ( ℤ≥ ‘ 3 )
2		1elfzo1ceilhalf1	⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
3	1 2	ax-mp	⊢ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
4	1 3	pm3.2i	⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
5		gpgusgra	⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 1 ) ∈ USGraph )
6		usgruspgr	⊢ ( ( 5 gPetersenGr 1 ) ∈ USGraph → ( 5 gPetersenGr 1 ) ∈ USPGraph )
7	4 5 6	mp2b	⊢ ( 5 gPetersenGr 1 ) ∈ USPGraph
8		pglem	⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
9	1 8	pm3.2i	⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
10		gpgusgra	⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 5 gPetersenGr 2 ) ∈ USGraph )
11		usgruspgr	⊢ ( ( 5 gPetersenGr 2 ) ∈ USGraph → ( 5 gPetersenGr 2 ) ∈ USPGraph )
12	9 10 11	mp2b	⊢ ( 5 gPetersenGr 2 ) ∈ USPGraph
13	7 12	pm3.2i	⊢ ( ( 5 gPetersenGr 1 ) ∈ USPGraph ∧ ( 5 gPetersenGr 2 ) ∈ USPGraph )
14		gpgprismgr4cyclex	⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 1 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) )
15	1 14	ax-mp	⊢ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 1 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 )
16		pg4cyclnex	⊢ ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 )
17	15 16	pm3.2i	⊢ ( ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 1 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) ∧ ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) )
18		cycldlenngric	⊢ ( ( ( 5 gPetersenGr 1 ) ∈ USPGraph ∧ ( 5 gPetersenGr 2 ) ∈ USPGraph ) → ( ( ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 1 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) ∧ ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ ( 5 gPetersenGr 2 ) ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 4 ) ) → ¬ ( 5 gPetersenGr 1 ) ≃𝑔𝑟 ( 5 gPetersenGr 2 ) ) )
19	13 17 18	mp2	⊢ ¬ ( 5 gPetersenGr 1 ) ≃𝑔𝑟 ( 5 gPetersenGr 2 )