P. 486 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48501-48600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	grlimgrtri 48501*	If one of two locally isomorphic graphs has a triangle, so does the other. The triangle in the other graph is not necessarily the image (𝐹 “ 𝑇) of the triangle 𝑇 in the first graph. (Contributed by AV, 24-Aug-2025.)
⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺))    ⇒   ⊢ (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻))
Theorem	brgrlic 48502	The relation "is locally isomorphic to" for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ (𝑅 GraphLocIso 𝑆) ≠ ∅)
Theorem	brgrilci 48503	Prove that two graphs are locally isomorphic by an explicit local isomorphism. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐹 ∈ (𝑅 GraphLocIso 𝑆) → 𝑅 ≃𝑙𝑔𝑟 𝑆)
Theorem	grlicrel 48504	The "is locally isomorphic to" relation for graphs is a relation. (Contributed by AV, 9-Jun-2025.)
⊢ Rel ≃𝑙𝑔𝑟
Theorem	grlicrcl 48505	Reverse closure of the "is locally isomorphic to" relation for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ≃𝑙𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgrlic2 48506*	Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))))
Theorem	grilcbri 48507*	Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))))
Theorem	dfgrlic3 48508*	Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝑓‘𝑣))    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑗(𝑗:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑗 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))))
Theorem	grilcbri2 48509*	Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝑓‘𝑋))    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ (𝑋 ∈ 𝑉 → ∃𝑗(𝑗:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑗 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))))
Theorem	grlicref 48510	Graph local isomorphism is reflexive for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑙𝑔𝑟 𝐺)
Theorem	grlicsym 48511	Graph local isomorphism is symmetric for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑙𝑔𝑟 𝑆 → 𝑆 ≃𝑙𝑔𝑟 𝐺))
Theorem	grlicsymb 48512	Graph local isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph) → (𝐴 ≃𝑙𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑙𝑔𝑟 𝐴))
Theorem	grlictr 48513	Graph local isomorphism is transitive. (Contributed by AV, 10-Jun-2025.)
⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → 𝑅 ≃𝑙𝑔𝑟 𝑇)
Theorem	grlicer 48514	Local isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 11-Jun-2025.)
⊢ ( ≃𝑙𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph
Theorem	grlicen 48515	Locally isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 11-Jun-2025.)
⊢ 𝐵 = (Vtx‘𝑅)    &   ⊢ 𝐶 = (Vtx‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶)
Theorem	gricgrlic 48516	Isomorphic hypergraphs are locally isomorphic. (Contributed by AV, 12-Jun-2025.) (Proof shortened by AV, 11-Jul-2025.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐺 ≃𝑔𝑟 𝐻 → 𝐺 ≃𝑙𝑔𝑟 𝐻))
Theorem	clnbgr3stgrgrlim 48517*	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 any bijection between the vertices is a local isomorphism between the two graphs. (Contributed by AV, 28-Dec-2025.)
⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟 (StarGr‘𝑁) ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟 (StarGr‘𝑁)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
Theorem	clnbgr3stgrgrlic 48518*	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 48519*	Lemma for usgrexmpl1 48520. (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 48520	𝐺 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 48521	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 48522	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 48523	𝐺 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 48524*	Lemma for usgrexmpl2 48525. (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 48525	𝐺 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 48526	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 48527	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 48528*	Lemma for usgrexmpl2nb0 48529 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 48529	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 48530	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 48531	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 48532	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 48533	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 48534	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 48535*	𝐺 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 48536	The graphs 𝐻 and 𝐺 are not isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 48523, whereas 𝐺 does not, see usgrexmpl2trifr 48535. (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 48537	The graphs 𝐻 and 𝐺 are not locally isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 48523, whereas 𝐺 does not, see usgrexmpl2trifr 48535. (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.48.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 48538	Extend class notation with generalized Petersen graphs.
class gPetersenGr
Definition	df-gpg 48539*	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 48540*	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 48541	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 48542*	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 48543*	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 48544*	Lemma for gpgiedgdmel 48547 and gpgedgel 48548. (Contributed by AV, 2-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (∃𝑥 ∈ 𝐼 (𝑌 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑌 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑌 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩}) → 𝑌 ∈ 𝒫 ({0, 1} × 𝐼)))
Theorem	gpgvtxel 48545*	A vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 29-Aug-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → (𝑋 ∈ 𝑉 ↔ ∃𝑥 ∈ {0, 1}∃𝑦 ∈ 𝐼 𝑋 = ⟨𝑥, 𝑦⟩))
Theorem	gpgvtxel2 48546	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 48547*	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 48548*	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 48549*	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 48550	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 48551	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 48552	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 48553	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 48554*	Lemma for gpgusgra 48555. (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 48555	The generalized Petersen graph GPG(N,K) is a simple graph. (Contributed by AV, 27-Aug-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (𝑁 gPetersenGr 𝐾) ∈ USGraph)
Theorem	gpgprismgrusgra 48556	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 48557	The order of the generalized Petersen graph GPG(N,K). (Contributed by AV, 29-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (♯‘(Vtx‘(𝑁 gPetersenGr 𝐾))) = (2 · 𝑁))
Theorem	gpg5order 48558	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 48559	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 48560	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 48561	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 48562	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 48563	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 48564	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 48565	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 48566	Lemma 1 for gpg5nbgrvtx03star 48578. (Contributed by AV, 5-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑊) → {⟨0, ((𝑋 + 1) mod 𝑁)⟩, ⟨1, 𝑋⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx03starlem2 48567	Lemma 2 for gpg5nbgrvtx03star 48578. (Contributed by AV, 6-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ ℤ) → {⟨0, ((𝑋 + 1) mod 𝑁)⟩, ⟨0, ((𝑋 − 1) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx03starlem3 48568	Lemma 3 for gpg5nbgrvtx03star 48578. (Contributed by AV, 5-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑊) → {⟨1, 𝑋⟩, ⟨0, ((𝑋 − 1) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem1 48569	Lemma 1 for gpg5nbgr3star 48579. (Contributed by AV, 7-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑊) → {⟨1, ((𝑋 + 𝐾) mod 𝑁)⟩, ⟨0, 𝑋⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem2 48570	Lemma 2 for gpg5nbgr3star 48579. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ ℤ) → {⟨1, ((𝑋 + 𝐾) mod 𝑁)⟩, ⟨1, ((𝑋 − 𝐾) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem3 48571	Lemma 3 for gpg5nbgr3star 48579. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑊) → {⟨0, 𝑋⟩, ⟨1, ((𝑋 − 𝐾) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpgnbgrvtx0 48572	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 48573	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 48574	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 48575	In a generalized Petersen graph 𝐺, every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025.) The proof of gpg3nbgrvtx0 48574 can be shortened using modmknepk 47838, but then theorem 2ltceilhalf 47802 is required which is based on an "example" ex-ceil 30543. 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 48576	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 48577	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 48580), i.e., every vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → (♯‘𝑈) = 3)
Theorem	gpg5nbgrvtx03star 48578*	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 48579*	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 48587. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → ((♯‘𝑈) = 3 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸))
Theorem	gpgvtxdg3 48580	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 48581	Lemma 1 for gpg3kgrtriex 48587. (Contributed by AV, 1-Oct-2025.)
⊢ (𝐾 ∈ ℕ → 𝐾 < (⌈‘((3 · 𝐾) / 2)))
Theorem	gpg3kgrtriexlem2 48582	Lemma 2 for gpg3kgrtriex 48587. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (-𝐾 mod 𝑁) = (((𝐾 mod 𝑁) + 𝐾) mod 𝑁))
Theorem	gpg3kgrtriexlem3 48583	Lemma 3 for gpg3kgrtriex 48587. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ (ℤ≥‘3))
Theorem	gpg3kgrtriexlem4 48584	Lemma 4 for gpg3kgrtriex 48587. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ (1..^(⌈‘(𝑁 / 2))))
Theorem	gpg3kgrtriexlem5 48585	Lemma 5 for gpg3kgrtriex 48587. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (𝐾 mod 𝑁) ≠ (-𝐾 mod 𝑁))
Theorem	gpg3kgrtriexlem6 48586	Lemma 6 for gpg3kgrtriex 48587: 𝐸 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 48587*	All generalized Petersen graphs G(N,K) with 𝑁 = 3 · 𝐾 contain triangles. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺))
Theorem	gpg5gricstgr3 48588	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 48589	Lemma for theorems about Petersen graphs. (Contributed by AV, 10-Nov-2025.)
⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
Theorem	pgjsgr 48590	A Petersen graph is a simple graph. (Contributed by AV, 10-Nov-2025.)
⊢ (5 gPetersenGr 2) ∈ USGraph
Theorem	gpg5grlim 48591	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 48592	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 48593	Lemma 1 for gpgprismgr4cycl0 48604: 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 48594	Lemma 2 for gpgprismgr4cycl0 48604: 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 48595*	Lemma 3 for gpgprismgr4cycl0 48604. (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 48596	Lemma 4 for gpgprismgr4cycl0 48604: the cycle ⟨𝑃, 𝐹⟩ consists of 5 vertices (the first and the last vertex are identical, see gpgprismgr4cycllem6 48598. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ (♯‘𝑃) = 5
Theorem	gpgprismgr4cycllem5 48597	Lemma 5 for gpgprismgr4cycl0 48604. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ 𝑃 ∈ Word V
Theorem	gpgprismgr4cycllem6 48598	Lemma 6 for gpgprismgr4cycl0 48604: 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 48599	Lemma 7 for gpgprismgr4cycl0 48604: 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 48600	Lemma 8 for gpgprismgr4cycl0 48604. (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‘𝐺))