P. 491 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49001-49100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clnbgr3stgrgrlic 49001*	If all (closed) neighborhoods of the vertices in two simple graphs with the same order induce a subgraph which is isomorphic to an 𝑁-star, then the two graphs are locally isomorphic. (Contributed by AV, 29-Sep-2025.)
⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟 (StarGr‘𝑁) ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟 (StarGr‘𝑁)) → 𝐺 ≃𝑙𝑔𝑟 𝐻)
Theorem	usgrexmpl1lem 49002*	Lemma for usgrexmpl1 49003. (Contributed by AV, 2-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    ⇒   ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
Theorem	usgrexmpl1 49003	𝐺 is a simple graph of six vertices 0, 1, 2, 3, 4, 5, with edges {0, 1}, {1, 2}, {0, 2}, {0, 3}, {3, 4}, {3, 5}, {4, 5}. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐺 ∈ USGraph
Theorem	usgrexmpl1vtx 49004	The vertices 0, 1, 2, 3, 4, 5 of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Vtx‘𝐺) = ({0, 1, 2} ∪ {3, 4, 5})
Theorem	usgrexmpl1edg 49005	The edges {0, 1}, {1, 2}, {0, 2}, {0, 3}, {3, 4}, {3, 5}, {4, 5} of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Edg‘𝐺) = ({{0, 3}} ∪ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4, 5}}))
Theorem	usgrexmpl1tri 49006	𝐺 contains a triangle 0, 1, 2, with corresponding edges {0, 1}, {1, 2}, {0, 2}. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ {0, 1, 2} ∈ (GrTriangles‘𝐺)
Theorem	usgrexmpl2lem 49007*	Lemma for usgrexmpl2 49008. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    ⇒   ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
Theorem	usgrexmpl2 49008	𝐺 is a simple graph of six vertices 0, 1, 2, 3, 4, 5, with edges {0, 1}, {1, 2}, {2, 3}, {0, 3}, {3, 4}, {4, 5}, {0, 5}. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐺 ∈ USGraph
Theorem	usgrexmpl2vtx 49009	The vertices 0, 1, 2, 3, 4, 5 of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Vtx‘𝐺) = ({0, 1, 2} ∪ {3, 4, 5})
Theorem	usgrexmpl2edg 49010	The edges {0, 1}, {1, 2}, {2, 3}, {0, 3}, {3, 4}, {4, 5}, {0, 5} of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Edg‘𝐺) = ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))
Theorem	usgrexmpl2nblem 49011*	Lemma for usgrexmpl2nb0 49012 etc. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐾 ∈ ({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 𝐾) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣ {𝐾, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))})
Theorem	usgrexmpl2nb0 49012	The neighborhood of the first vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 0) = {1, 3, 5}
Theorem	usgrexmpl2nb1 49013	The neighborhood of the second vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 1) = {0, 2}
Theorem	usgrexmpl2nb2 49014	The neighborhood of the third vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 2) = {1, 3}
Theorem	usgrexmpl2nb3 49015	The neighborhood of the forth vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 3) = {0, 2, 4}
Theorem	usgrexmpl2nb4 49016	The neighborhood of the fifth vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 4) = {3, 5}
Theorem	usgrexmpl2nb5 49017	The neighborhood of the sixth vertex of graph 𝐺. (Contributed by AV, 10-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 5) = {0, 4}
Theorem	usgrexmpl2trifr 49018*	𝐺 is triangle-free. (Contributed by AV, 10-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ¬ ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺)
Theorem	usgrexmpl12ngric 49019	The graphs 𝐻 and 𝐺 are not isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 49006, whereas 𝐺 does not, see usgrexmpl2trifr 49018. (Contributed by AV, 10-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    &   ⊢ 𝐾 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐻 = ⟨𝑉, 𝐾⟩    ⇒   ⊢ ¬ 𝐺 ≃𝑔𝑟 𝐻
Theorem	usgrexmpl12ngrlic 49020	The graphs 𝐻 and 𝐺 are not locally isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 49006, whereas 𝐺 does not, see usgrexmpl2trifr 49018. (Contributed by AV, 24-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    &   ⊢ 𝐾 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐻 = ⟨𝑉, 𝐾⟩    ⇒   ⊢ ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻
21.50.15.8  Generalized Petersen graphs According to Wikipedia "Generalized Petersen graph", 26-Aug-2025, https://en.wikipedia.org/wiki/Generalized_Petersen_graph: "In graph theory, the generalized Petersen graphs are a family of cubic graphs formed by connecting the vertices of a regular polygon to the corresponding vertices of a star polygon. They include the Petersen graph and generalize one of the ways of constructing the Petersen graph. ... Among the generalized Petersen graphs are the n-prism, ...". The vertices of the regular polygon are called "outside vertices", the vertices of the star polygon "inside vertices" (see A. Steimle, W. Stanton, "The isomorphism classes of the generalized Petersen graphs", Discrete Mathematics Volume 309, Issue 1, 6 January 2009, Pages 231-237: https://doi.org/10.1016/j.disc.2007.12.074). Since regular polygons are also considered as star polygons (with density 1), many theorems for "inside vertices" (with labels containing the fragment "vtx1") can be specialized for "outside vertices" (with labels containing the fragment "vtx0").
Syntax	cgpg 49021	Extend class notation with generalized Petersen graphs.
class gPetersenGr
Definition	df-gpg 49022*	Definition of generalized Petersen graphs according to Wikipedia "Generalized Petersen graph", 26-Aug-2025, https://en.wikipedia.org/wiki/Generalized_Petersen_graph: "In Watkins' notation, 𝐺(𝑛, 𝑘) is a graph with vertex set { u0, u1, ... , un-1, v0, v1, ... , vn-1 } and edge set { ui ui+1 , ui vi , vi vi+k | 0 ≤ 𝑖 ≤ (𝑛 − 1) } where subscripts are to be read modulo n and where 𝑘 < (𝑛 / 2). Some authors use the notation GPG(n,k)." Instead of 𝑛 ∈ ℕ, we could restrict the first argument to 𝑛 ∈ (ℤ≥‘3) (i.e., 3 ≤ 𝑛), because for 𝑛 ≤ 2, the definition is not meaningful (since then (⌈‘(𝑛 / 2)) ≤ 1 and therefore (1..^(⌈‘(𝑛 / 2))) = ∅, so that there would be no fitting second argument). (Contributed by AV, 26-Aug-2025.)
⊢ gPetersenGr = (𝑛 ∈ ℕ, 𝑘 ∈ (1..^(⌈‘(𝑛 / 2))) ↦ {⟨(Base‘ndx), ({0, 1} × (0..^𝑛))⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})})⟩})
Theorem	gpgov 49023*	The generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (𝑁 gPetersenGr 𝐾) = {⟨(Base‘ndx), ({0, 1} × 𝐼)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})⟩})
Theorem	gpgvtx 49024	The vertices of the generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (Vtx‘(𝑁 gPetersenGr 𝐾)) = ({0, 1} × 𝐼))
Theorem	gpgiedg 49025*	The indexed edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (iEdg‘(𝑁 gPetersenGr 𝐾)) = ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})}))
Theorem	gpgedg 49026*	The edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (Edg‘(𝑁 gPetersenGr 𝐾)) = {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})
Theorem	gpgiedgdmellem 49027*	Lemma for gpgiedgdmel 49030 and gpgedgel 49031. (Contributed by AV, 2-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (∃𝑥 ∈ 𝐼 (𝑌 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑌 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑌 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩}) → 𝑌 ∈ 𝒫 ({0, 1} × 𝐼)))
Theorem	gpgvtxel 49028*	A vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 29-Aug-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → (𝑋 ∈ 𝑉 ↔ ∃𝑥 ∈ {0, 1}∃𝑦 ∈ 𝐼 𝑋 = ⟨𝑥, 𝑦⟩))
Theorem	gpgvtxel2 49029	The second component of a vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 30-Aug-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑉) → (2nd ‘𝑋) ∈ 𝐼)
Theorem	gpgiedgdmel 49030*	An index of edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 2-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (𝑋 ∈ dom (iEdg‘𝐺) ↔ ∃𝑥 ∈ 𝐼 (𝑋 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑋 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑋 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})))
Theorem	gpgedgel 49031*	An edge in a generalized Petersen graph 𝐺. (Contributed by AV, 29-Aug-2025.) (Proof shortened by AV, 8-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → (𝑌 ∈ 𝐸 ↔ ∃𝑥 ∈ 𝐼 (𝑌 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑌 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑌 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})))
Theorem	gpgprismgriedgdmel 49032*	An index of edges of the generalized Petersen graph GPG(N,1). (Contributed by AV, 2-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 1)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑋 ∈ dom (iEdg‘𝐺) ↔ ∃𝑥 ∈ 𝐼 (𝑋 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑋 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑋 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
Theorem	gpgprismgriedgdmss 49033	A subset of the index of edges of the generalized Petersen graph GPG(N,1). (Contributed by AV, 2-Nov-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → ({{⟨0, 0⟩, ⟨0, 1⟩}, {⟨0, 0⟩, ⟨1, 0⟩}} ∪ {{⟨1, 1⟩, ⟨0, 1⟩}, {⟨1, 1⟩, ⟨1, 0⟩}}) ⊆ dom (iEdg‘(𝑁 gPetersenGr 1)))
Theorem	gpgvtx0 49034	The outside vertices in a generalized Petersen graph 𝐺. (Contributed by AV, 30-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑉) → (⟨0, (((2nd ‘𝑋) + 1) mod 𝑁)⟩ ∈ 𝑉 ∧ ⟨0, (2nd ‘𝑋)⟩ ∈ 𝑉 ∧ ⟨0, (((2nd ‘𝑋) − 1) mod 𝑁)⟩ ∈ 𝑉))
Theorem	gpgvtx1 49035	The inside vertices in a generalized Petersen graph 𝐺. (Contributed by AV, 28-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑉) → (⟨1, (((2nd ‘𝑋) + 𝐾) mod 𝑁)⟩ ∈ 𝑉 ∧ ⟨1, (2nd ‘𝑋)⟩ ∈ 𝑉 ∧ ⟨1, (((2nd ‘𝑋) − 𝐾) mod 𝑁)⟩ ∈ 𝑉))
Theorem	opgpgvtx 49036	A vertex in a generalized Petersen graph 𝐺 as ordered pair. (Contributed by AV, 1-Oct-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → (⟨𝑋, 𝑌⟩ ∈ 𝑉 ↔ ((𝑋 = 0 ∨ 𝑋 = 1) ∧ 𝑌 ∈ 𝐼)))
Theorem	gpgusgralem 49037*	Lemma for gpgusgra 49038. (Contributed by AV, 27-Aug-2025.) (Proof shortened by AV, 6-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})} ⊆ {𝑝 ∈ 𝒫 ({0, 1} × 𝐼) ∣ (♯‘𝑝) = 2})
Theorem	gpgusgra 49038	The generalized Petersen graph GPG(N,K) is a simple graph. (Contributed by AV, 27-Aug-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (𝑁 gPetersenGr 𝐾) ∈ USGraph)
Theorem	gpgprismgrusgra 49039	The generalized Petersen graphs G(N,1), which are the N-prisms, are simple graphs. (Contributed by AV, 31-Oct-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 gPetersenGr 1) ∈ USGraph)
Theorem	gpgorder 49040	The order of the generalized Petersen graph GPG(N,K). (Contributed by AV, 29-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (♯‘(Vtx‘(𝑁 gPetersenGr 𝐾))) = (2 · 𝑁))
Theorem	gpg5order 49041	The order of a generalized Petersen graph G(5,K), which is either the Petersen graph G(5,2) or the 5-prism G(5,1), is 10. (Contributed by AV, 26-Aug-2025.)
⊢ (𝐾 ∈ (1...2) → (♯‘(Vtx‘(5 gPetersenGr 𝐾))) = ;10)
Theorem	gpgedgvtx0 49042	The edges starting at an outside vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 29-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝑉 ∧ (1st ‘𝑋) = 0)) → ({𝑋, ⟨0, (((2nd ‘𝑋) + 1) mod 𝑁)⟩} ∈ 𝐸 ∧ {𝑋, ⟨1, (2nd ‘𝑋)⟩} ∈ 𝐸 ∧ {𝑋, ⟨0, (((2nd ‘𝑋) − 1) mod 𝑁)⟩} ∈ 𝐸))
Theorem	gpgedgvtx1 49043	The edges starting at an inside vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 2-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝑉 ∧ (1st ‘𝑋) = 1)) → ({𝑋, ⟨1, (((2nd ‘𝑋) + 𝐾) mod 𝑁)⟩} ∈ 𝐸 ∧ {𝑋, ⟨0, (2nd ‘𝑋)⟩} ∈ 𝐸 ∧ {𝑋, ⟨1, (((2nd ‘𝑋) − 𝐾) mod 𝑁)⟩} ∈ 𝐸))
Theorem	gpgvtxedg0 49044	The edges starting at an outside vertex 𝑋 in a generalized Petersen graph 𝐺. (Contributed by AV, 30-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (1st ‘𝑋) = 0 ∧ {𝑋, 𝑌} ∈ 𝐸) → (𝑌 = ⟨0, (((2nd ‘𝑋) + 1) mod 𝑁)⟩ ∨ 𝑌 = ⟨1, (2nd ‘𝑋)⟩ ∨ 𝑌 = ⟨0, (((2nd ‘𝑋) − 1) mod 𝑁)⟩))
Theorem	gpgvtxedg1 49045	The edges starting at an inside vertex 𝑋 in a generalized Petersen graph 𝐺. (Contributed by AV, 2-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (1st ‘𝑋) = 1 ∧ {𝑋, 𝑌} ∈ 𝐸) → (𝑌 = ⟨1, (((2nd ‘𝑋) + 𝐾) mod 𝑁)⟩ ∨ 𝑌 = ⟨0, (2nd ‘𝑋)⟩ ∨ 𝑌 = ⟨1, (((2nd ‘𝑋) − 𝐾) mod 𝑁)⟩))
Theorem	gpgedgiov 49046	The edges of the generalized Petersen graph GPG(N,K) between an inside and an outside vertex. (Contributed by AV, 11-Nov-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → ({⟨0, 𝑋⟩, ⟨1, 𝑌⟩} ∈ 𝐸 ↔ 𝑋 = 𝑌))
Theorem	gpgedg2ov 49047	The edges of the generalized Petersen graph GPG(N,K) between two outside vertices. (Contributed by AV, 15-Nov-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘5) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼)) → (({⟨0, ((𝑌 − 1) mod 𝑁)⟩, ⟨0, 𝑋⟩} ∈ 𝐸 ∧ {⟨0, 𝑋⟩, ⟨0, ((𝑌 + 1) mod 𝑁)⟩} ∈ 𝐸) ↔ 𝑋 = 𝑌))
Theorem	gpgedg2iv 49048	The edges of the generalized Petersen graph GPG(N,K) between two inside vertices. (Contributed by AV, 20-Nov-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘5) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ (𝐾 ∈ 𝐽 ∧ ((4 · 𝐾) mod 𝑁) ≠ 0)) → (({⟨1, ((𝑌 − 𝐾) mod 𝑁)⟩, ⟨1, 𝑋⟩} ∈ 𝐸 ∧ {⟨1, 𝑋⟩, ⟨1, ((𝑌 + 𝐾) mod 𝑁)⟩} ∈ 𝐸) ↔ 𝑋 = 𝑌))
Theorem	gpg5nbgrvtx03starlem1 49049	Lemma 1 for gpg5nbgrvtx03star 49061. (Contributed by AV, 5-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑊) → {⟨0, ((𝑋 + 1) mod 𝑁)⟩, ⟨1, 𝑋⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx03starlem2 49050	Lemma 2 for gpg5nbgrvtx03star 49061. (Contributed by AV, 6-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ ℤ) → {⟨0, ((𝑋 + 1) mod 𝑁)⟩, ⟨0, ((𝑋 − 1) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx03starlem3 49051	Lemma 3 for gpg5nbgrvtx03star 49061. (Contributed by AV, 5-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑊) → {⟨1, 𝑋⟩, ⟨0, ((𝑋 − 1) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem1 49052	Lemma 1 for gpg5nbgr3star 49062. (Contributed by AV, 7-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑊) → {⟨1, ((𝑋 + 𝐾) mod 𝑁)⟩, ⟨0, 𝑋⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem2 49053	Lemma 2 for gpg5nbgr3star 49062. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ ℤ) → {⟨1, ((𝑋 + 𝐾) mod 𝑁)⟩, ⟨1, ((𝑋 − 𝐾) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem3 49054	Lemma 3 for gpg5nbgr3star 49062. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑊) → {⟨0, 𝑋⟩, ⟨1, ((𝑋 − 𝐾) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpgnbgrvtx0 49055	The (open) neighborhood of an outside vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 28-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝑉 ∧ (1st ‘𝑋) = 0)) → 𝑈 = {⟨0, (((2nd ‘𝑋) + 1) mod 𝑁)⟩, ⟨1, (2nd ‘𝑋)⟩, ⟨0, (((2nd ‘𝑋) − 1) mod 𝑁)⟩})
Theorem	gpgnbgrvtx1 49056	The (open) neighborhood of an inside vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 2-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝑉 ∧ (1st ‘𝑋) = 1)) → 𝑈 = {⟨1, (((2nd ‘𝑋) + 𝐾) mod 𝑁)⟩, ⟨0, (2nd ‘𝑋)⟩, ⟨1, (((2nd ‘𝑋) − 𝐾) mod 𝑁)⟩})
Theorem	gpg3nbgrvtx0 49057	In a generalized Petersen graph 𝐺, every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝑉 ∧ (1st ‘𝑋) = 0)) → (♯‘𝑈) = 3)
Theorem	gpg3nbgrvtx0ALT 49058	In a generalized Petersen graph 𝐺, every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025.) The proof of gpg3nbgrvtx0 49057 can be shortened using modmknepk 48321, but then theorem 2ltceilhalf 48285 is required which is based on an "example" ex-ceil 30960. If these theorems were moved to main, the "example" should also be moved up to become a full-fledged theorem. (Proof shortened by AV, 4-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝑉 ∧ (1st ‘𝑋) = 0)) → (♯‘𝑈) = 3)
Theorem	gpg3nbgrvtx1 49059	In a generalized Petersen graph 𝐺, every inside vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025.) (Proof shortened by AV, 22-Nov-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝑉 ∧ (1st ‘𝑋) = 1)) → (♯‘𝑈) = 3)
Theorem	gpgcubic 49060	Every generalized Petersen graph is a cubic graph, i.e., it is a 3-regular graph, i.e., every vertex has degree 3 (see gpgvtxdg3 49063), i.e., every vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → (♯‘𝑈) = 3)
Theorem	gpg5nbgrvtx03star 49061*	In a generalized Petersen graph G(N,K) of order greater than 8 (3 < 𝑁), every outside vertex has exactly three (different) neighbors, and none of these neighbors are connected by an edge (i.e., the (closed) neighborhood of every outside vertex induces a subgraph which is isomorphic to a 3-star). (Contributed by AV, 31-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘4) ∧ 𝐾 ∈ 𝐽) ∧ (𝑋 ∈ 𝑉 ∧ (1st ‘𝑋) = 0)) → ((♯‘𝑈) = 3 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸))
Theorem	gpg5nbgr3star 49062*	In a generalized Petersen graph G(N,K) of order 10 (𝑁 = 5), these are the Petersen graph G(5,2) and the 5-prism G(5,1), every vertex has exactly three (different) neighbors, and none of these neighbors are connected by an edge (i.e., the (closed) neighborhood of every vertex induces a subgraph which is isomorphic to a 3-star). This does not hold for every generalized Petersen graph: for example, in the 3-prism G(3,1) (see gpg31grim3prism TODO) and the Dürer graph G(6,2) there are vertices which have neighborhoods containing triangles. In general, all generalized Petersen graphs G(N,K) with 𝑁 = 3 · 𝐾 contain triangles, see gpg3kgrtriex 49070. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → ((♯‘𝑈) = 3 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸))
Theorem	gpgvtxdg3 49063	Every vertex in a generalized Petersen graph has degree 3. (Contributed by AV, 4-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑋) = 3)
Theorem	gpg3kgrtriexlem1 49064	Lemma 1 for gpg3kgrtriex 49070. (Contributed by AV, 1-Oct-2025.)
⊢ (𝐾 ∈ ℕ → 𝐾 < (⌈‘((3 · 𝐾) / 2)))
Theorem	gpg3kgrtriexlem2 49065	Lemma 2 for gpg3kgrtriex 49070. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (-𝐾 mod 𝑁) = (((𝐾 mod 𝑁) + 𝐾) mod 𝑁))
Theorem	gpg3kgrtriexlem3 49066	Lemma 3 for gpg3kgrtriex 49070. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ (ℤ≥‘3))
Theorem	gpg3kgrtriexlem4 49067	Lemma 4 for gpg3kgrtriex 49070. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ (1..^(⌈‘(𝑁 / 2))))
Theorem	gpg3kgrtriexlem5 49068	Lemma 5 for gpg3kgrtriex 49070. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (𝐾 mod 𝑁) ≠ (-𝐾 mod 𝑁))
Theorem	gpg3kgrtriexlem6 49069	Lemma 6 for gpg3kgrtriex 49070: 𝐸 is an edge in the generalized Petersen graph G(N,K) with 𝑁 = 3 · 𝐾. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝐸 = {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩}    ⇒   ⊢ (𝐾 ∈ ℕ → 𝐸 ∈ (Edg‘𝐺))
Theorem	gpg3kgrtriex 49070*	All generalized Petersen graphs G(N,K) with 𝑁 = 3 · 𝐾 contain triangles. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺))
Theorem	gpg5gricstgr3 49071	Each closed neighborhood in a generalized Petersen graph G(N,K) of order 10 (𝑁 = 5), which is either the Petersen graph G(5,2) or the 5-prism G(5,1), is isomorphic to a 3-star. (Contributed by AV, 13-Sep-2025.)
⊢ 𝐺 = (5 gPetersenGr 𝐾)    ⇒   ⊢ ((𝐾 ∈ (1...2) ∧ 𝑉 ∈ (Vtx‘𝐺)) → (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑉)) ≃𝑔𝑟 (StarGr‘3))
Theorem	pglem 49072	Lemma for theorems about Petersen graphs. (Contributed by AV, 10-Nov-2025.)
⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
Theorem	pgjsgr 49073	A Petersen graph is a simple graph. (Contributed by AV, 10-Nov-2025.)
⊢ (5 gPetersenGr 2) ∈ USGraph
Theorem	gpg5grlim 49074	A local isomorphism between the two generalized Petersen graphs G(N,K) of order 10 (𝑁 = 5), which are the Petersen graph G(5,2) and the 5-prism G(5,1). (Contributed by AV, 28-Dec-2025.)
⊢ ( I ↾ ({0, 1} × (0..^5))) ∈ ((5 gPetersenGr 1) GraphLocIso (5 gPetersenGr 2))
Theorem	gpg5grlic 49075	The two generalized Petersen graphs G(N,K) of order 10 (𝑁 = 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.)
⊢ (5 gPetersenGr 1) ≃𝑙𝑔𝑟 (5 gPetersenGr 2)
Theorem	gpgprismgr4cycllem1 49076	Lemma 1 for gpgprismgr4cycl0 49087: the cycle ⟨𝑃, 𝐹⟩ consists of 4 edges (i.e., has length 4). (Contributed by AV, 1-Nov-2025.)
⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩    ⇒   ⊢ (♯‘𝐹) = 4
Theorem	gpgprismgr4cycllem2 49077	Lemma 2 for gpgprismgr4cycl0 49087: the cycle ⟨𝑃, 𝐹⟩ is proper, i.e., it has no overlapping edges. (Contributed by AV, 2-Nov-2025.)
⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩    ⇒   ⊢ Fun ◡𝐹
Theorem	gpgprismgr4cycllem3 49078*	Lemma 3 for gpgprismgr4cycl0 49087. (Contributed by AV, 5-Nov-2025.)
⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑋 ∈ (0..^4)) → ((𝐹‘𝑋) ∈ 𝒫 ({0, 1} × (0..^𝑁)) ∧ ∃𝑥 ∈ (0..^𝑁)((𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ (𝐹‘𝑋) = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ (𝐹‘𝑋) = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
Theorem	gpgprismgr4cycllem4 49079	Lemma 4 for gpgprismgr4cycl0 49087: the cycle ⟨𝑃, 𝐹⟩ consists of 5 vertices (the first and the last vertex are identical, see gpgprismgr4cycllem6 49081. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ (♯‘𝑃) = 5
Theorem	gpgprismgr4cycllem5 49080	Lemma 5 for gpgprismgr4cycl0 49087. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ 𝑃 ∈ Word V
Theorem	gpgprismgr4cycllem6 49081	Lemma 6 for gpgprismgr4cycl0 49087: the cycle ⟨𝑃, 𝐹⟩ is closed, i.e., the first and the last vertex are identical. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ (𝑃‘0) = (𝑃‘4)
Theorem	gpgprismgr4cycllem7 49082	Lemma 7 for gpgprismgr4cycl0 49087: the cycle ⟨𝑃, 𝐹⟩ is proper, i.e., it has no overlapping vertices, except the first and the last one. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ ((𝑋 ∈ (0..^(♯‘𝑃)) ∧ 𝑌 ∈ (1..^4)) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
Theorem	gpgprismgr4cycllem8 49083	Lemma 8 for gpgprismgr4cycl0 49087. (Contributed by AV, 2-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    &   ⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩    &   ⊢ 𝐺 = (𝑁 gPetersenGr 1)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝐹 ∈ Word dom (iEdg‘𝐺))
Theorem	gpgprismgr4cycllem9 49084	Lemma 9 for gpgprismgr4cycl0 49087. (Contributed by AV, 3-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    &   ⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩    &   ⊢ 𝐺 = (𝑁 gPetersenGr 1)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))
Theorem	gpgprismgr4cycllem10 49085	Lemma 10 for gpgprismgr4cycl0 49087. (Contributed by AV, 5-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    &   ⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩    &   ⊢ 𝐺 = (𝑁 gPetersenGr 1)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑋 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑋)) = {(𝑃‘𝑋), (𝑃‘(𝑋 + 1))})
Theorem	gpgprismgr4cycllem11 49086	Lemma 11 for gpgprismgr4cycl0 49087. (Contributed by AV, 5-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    &   ⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩    &   ⊢ 𝐺 = (𝑁 gPetersenGr 1)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝐹(Cycles‘𝐺)𝑃)
Theorem	gpgprismgr4cycl0 49087	The generalized Petersen graphs G(N,1), which are the N-prisms, have a cycle of length 4 starting at the vertex ⟨0, 0⟩. (Contributed by AV, 5-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    &   ⊢ 𝐹 = ⟨“{⟨0, 0⟩, ⟨0, 1⟩} {⟨0, 1⟩, ⟨1, 1⟩} {⟨1, 1⟩, ⟨1, 0⟩} {⟨1, 0⟩, ⟨0, 0⟩}”⟩    &   ⊢ 𝐺 = (𝑁 gPetersenGr 1)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘3) → (𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 4))
Theorem	gpgprismgr4cyclex 49088*	The generalized Petersen graphs G(N,1), which are the N-prisms, have (at least) one cycle of length 4. (Contributed by AV, 5-Nov-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → ∃𝑝∃𝑓(𝑓(Cycles‘(𝑁 gPetersenGr 1))𝑝 ∧ (♯‘𝑓) = 4))
Theorem	pgnioedg1 49089	An inside and an outside vertex not adjacent in a Petersen graph. (Contributed by AV, 21-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑦 ∈ (0..^5) → ¬ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, ((𝑦 + 1) mod 5)⟩} ∈ 𝐸)
Theorem	pgnioedg2 49090	An inside and an outside vertex not adjacent in a Petersen graph. (Contributed by AV, 21-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑦 ∈ (0..^5) → ¬ {⟨1, ((𝑦 + 2) mod 5)⟩, ⟨0, ((𝑦 + 1) mod 5)⟩} ∈ 𝐸)
Theorem	pgnioedg3 49091	An inside and an outside vertex not adjacent in a Petersen graph. (Contributed by AV, 21-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑦 ∈ (0..^5) → ¬ {⟨1, ((𝑦 + 2) mod 5)⟩, ⟨0, ((𝑦 − 1) mod 5)⟩} ∈ 𝐸)
Theorem	pgnioedg4 49092	An inside and an outside vertex not adjacent in a Petersen graph. (Contributed by AV, 21-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑦 ∈ (0..^5) → ¬ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, ((𝑦 − 1) mod 5)⟩} ∈ 𝐸)
Theorem	pgnioedg5 49093	An inside and an outside vertex not adjacent in a Petersen graph. (Contributed by AV, 21-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑦 ∈ (0..^5) → ¬ {⟨1, ((𝑦 − 1) mod 5)⟩, ⟨0, ((𝑦 + 1) mod 5)⟩} ∈ 𝐸)
Theorem	pgnbgreunbgrlem1 49094*	Lemma 1 for pgnbgreunbgr 49106. (Contributed by AV, 15-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝐿 = ⟨0, (((2nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, (2nd ‘𝑋)⟩ ∨ 𝐿 = ⟨0, (((2nd ‘𝑋) − 1) mod 5)⟩) → ((𝐾 = ⟨0, (((2nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, (2nd ‘𝑋)⟩ ∨ 𝐾 = ⟨0, (((2nd ‘𝑋) − 1) mod 5)⟩) → ((𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨0, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ∧ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨0, 𝑏⟩)))))
Theorem	pgnbgreunbgrlem2lem1 49095*	Lemma 1 for pgnbgreunbgrlem2 49098. (Contributed by AV, 16-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨0, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨0, 𝑏⟩} ∈ 𝐸) → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸)
Theorem	pgnbgreunbgrlem2lem2 49096*	Lemma 2 for pgnbgreunbgrlem2 49098. (Contributed by AV, 16-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((((𝐿 = ⟨1, ((𝑦 − 2) mod 5)⟩ ∧ 𝐾 = ⟨0, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨0, 𝑏⟩} ∈ 𝐸) → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸)
Theorem	pgnbgreunbgrlem2lem3 49097*	Lemma 3 for pgnbgreunbgrlem2 49098. (Contributed by AV, 17-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨0, 𝑏⟩} ∈ 𝐸) → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸)
Theorem	pgnbgreunbgrlem2 49098*	Lemma 2 for pgnbgreunbgr 49106. Impossible cases. (Contributed by AV, 18-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝐿 = ⟨1, (((2nd ‘𝑋) + 2) mod 5)⟩ ∨ 𝐿 = ⟨0, (2nd ‘𝑋)⟩ ∨ 𝐿 = ⟨1, (((2nd ‘𝑋) − 2) mod 5)⟩) → ((𝐾 = ⟨1, (((2nd ‘𝑋) + 2) mod 5)⟩ ∨ 𝐾 = ⟨0, (2nd ‘𝑋)⟩ ∨ 𝐾 = ⟨1, (((2nd ‘𝑋) − 2) mod 5)⟩) → ((𝑋 = ⟨1, 𝑦⟩ ∧ 𝑋 ∈ 𝑉) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ∧ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨0, 𝑏⟩)))))
Theorem	pgnbgreunbgrlem3 49099	Lemma 3 for pgnbgreunbgr 49106. (Contributed by AV, 18-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿) ∧ 𝑏 ∈ (0..^5)) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ∧ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨0, 𝑏⟩))
Theorem	pgnbgreunbgrlem4 49100*	Lemma 4 for pgnbgreunbgr 49106. (Contributed by AV, 20-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝐿 = ⟨1, (((2nd ‘𝑋) + 2) mod 5)⟩ ∨ 𝐿 = ⟨0, (2nd ‘𝑋)⟩ ∨ 𝐿 = ⟨1, (((2nd ‘𝑋) − 2) mod 5)⟩) → ((𝐾 = ⟨1, (((2nd ‘𝑋) + 2) mod 5)⟩ ∨ 𝐾 = ⟨0, (2nd ‘𝑋)⟩ ∨ 𝐾 = ⟨1, (((2nd ‘𝑋) − 2) mod 5)⟩) → ((𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))))