P. 494 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49301-49400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	grlimpredg 49301*	For two locally isomorphic graphs 𝐺 and 𝐻 and a vertex 𝐴 of 𝐺 there is a bijection 𝑓 mapping the closed neighborhood 𝑁 of 𝐴 onto the closed neighborhood 𝑀 of (𝐹‘𝐴), so that the mapped vertices of an edge {𝐴, 𝐵} containing the vertex 𝐴 is an edge in 𝐻. (Contributed by AV, 27-Dec-2025.)
⊢ 𝑁 = (𝐺 ClNeighbVtx 𝐴)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝐴))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ {𝐴, 𝐵} ∈ 𝐼)) → ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ {(𝑓‘𝐴), (𝑓‘𝐵)} ∈ 𝐽))
Theorem	grlimprclnbgrvtx 49302*	For two locally isomorphic graphs 𝐺 and 𝐻 and a vertex 𝐴 of 𝐺 there is a bijection 𝑓 mapping the closed neighborhood 𝑁 of 𝐴 onto the closed neighborhood 𝑀 of (𝐹‘𝐴), so that the mapped vertices of an edge {𝐴, 𝐵} containing the vertex 𝐴 is an edge between the vertices in 𝑀 containing the vertex (𝐹‘𝐴). (Contributed by AV, 28-Dec-2025.)
⊢ 𝑁 = (𝐺 ClNeighbVtx 𝐴)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝐴))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ {𝐴, 𝐵} ∈ 𝐼)) → ∃𝑓(𝑓:𝑁⟶1-1onto𝑀 ∧ ({(𝐹‘𝐴), (𝑓‘𝐵)} ∈ 𝐿 ∨ {(𝐹‘𝐴), (𝑓‘𝐴)} ∈ 𝐿)))
Theorem	grlimgredgex 49303*	Local isomorphisms between simple pseudographs map an edge onto an edge with an endpoint being the image of one of the endpoints of the first edge under the local isomorphism. (Contributed by AV, 28-Dec-2025.)
⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝐼)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ 𝑉 {(𝐹‘𝐴), 𝑣} ∈ 𝐸)
Theorem	grlimgrtrilem1 49304*	Lemma 3 for grlimgrtri 49306. (Contributed by AV, 24-Aug-2025.) (Proof shortened by AV, 27-Dec-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ 𝐼 ∧ {𝑎, 𝑐} ∈ 𝐼 ∧ {𝑏, 𝑐} ∈ 𝐼)) → ({𝑎, 𝑏} ∈ 𝐾 ∧ {𝑎, 𝑐} ∈ 𝐾 ∧ {𝑏, 𝑐} ∈ 𝐾))
Theorem	grlimgrtrilem2 49305*	Lemma 3 for grlimgrtri 49306. (Contributed by AV, 23-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑎))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝑓:𝑁⟶1-1onto𝑀 ∧ 𝑔:𝐾⟶1-1onto𝐿) ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ 𝐾) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ 𝐽)
Theorem	grlimgrtri 49306*	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 49307	The relation "is locally isomorphic to" for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ (𝑅 GraphLocIso 𝑆) ≠ ∅)
Theorem	brgrilci 49308	Prove that two graphs are locally isomorphic by an explicit local isomorphism. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐹 ∈ (𝑅 GraphLocIso 𝑆) → 𝑅 ≃𝑙𝑔𝑟 𝑆)
Theorem	grlicrel 49309	The "is locally isomorphic to" relation for graphs is a relation. (Contributed by AV, 9-Jun-2025.)
⊢ Rel ≃𝑙𝑔𝑟
Theorem	grlicrcl 49310	Reverse closure of the "is locally isomorphic to" relation for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ≃𝑙𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgrlic2 49311*	Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉⟶1-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))))
Theorem	grilcbri 49312*	Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉⟶1-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))))
Theorem	dfgrlic3 49313*	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-1onto𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑗(𝑗:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑗 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))))
Theorem	grilcbri2 49314*	Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝑓‘𝑋))    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉⟶1-1onto𝑊 ∧ (𝑋 ∈ 𝑉 → ∃𝑗(𝑗:𝑁⟶1-1onto𝑀 ∧ ∃𝑔(𝑔:𝐾⟶1-1onto𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑗 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))))
Theorem	grlicref 49315	Graph local isomorphism is reflexive for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑙𝑔𝑟 𝐺)
Theorem	grlicsym 49316	Graph local isomorphism is symmetric for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑙𝑔𝑟 𝑆 → 𝑆 ≃𝑙𝑔𝑟 𝐺))
Theorem	grlicsymb 49317	Graph local isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph) → (𝐴 ≃𝑙𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑙𝑔𝑟 𝐴))
Theorem	grlictr 49318	Graph local isomorphism is transitive. (Contributed by AV, 10-Jun-2025.)
⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → 𝑅 ≃𝑙𝑔𝑟 𝑇)
Theorem	grlicer 49319	Local isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 11-Jun-2025.)
⊢ ( ≃𝑙𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph
Theorem	grlicen 49320	Locally isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 11-Jun-2025.)
⊢ 𝐵 = (Vtx‘𝑅)    &   ⊢ 𝐶 = (Vtx‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶)
Theorem	gricgrlic 49321	Isomorphic hypergraphs are locally isomorphic. (Contributed by AV, 12-Jun-2025.) (Proof shortened by AV, 11-Jul-2025.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐺 ≃𝑔𝑟 𝐻 → 𝐺 ≃𝑙𝑔𝑟 𝐻))
Theorem	clnbgr3stgrgrlim 49322*	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-1onto𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟 (StarGr‘𝑁) ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟 (StarGr‘𝑁)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
Theorem	clnbgr3stgrgrlic 49323*	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 49324*	Lemma for usgrexmpl1 49325. (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 49325	𝐺 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 49326	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 49327	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 49328	𝐺 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 49329*	Lemma for usgrexmpl2 49330. (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 49330	𝐺 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 49331	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 49332	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 49333*	Lemma for usgrexmpl2nb0 49334 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 49334	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 49335	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 49336	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 49337	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 49338	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 49339	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 49340*	𝐺 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 49341	The graphs 𝐻 and 𝐺 are not isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 49328, whereas 𝐺 does not, see usgrexmpl2trifr 49340. (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 49342	The graphs 𝐻 and 𝐺 are not locally isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 49328, whereas 𝐺 does not, see usgrexmpl2trifr 49340. (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.52.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 49343	Extend class notation with generalized Petersen graphs.
class gPetersenGr
Definition	df-gpg 49344*	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 49345*	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 49346	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 49347*	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 49348*	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 49349*	Lemma for gpgiedgdmel 49352 and gpgedgel 49353. (Contributed by AV, 2-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (∃𝑥 ∈ 𝐼 (𝑌 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑌 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑌 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩}) → 𝑌 ∈ 𝒫 ({0, 1} × 𝐼)))
Theorem	gpgvtxel 49350*	A vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 29-Aug-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → (𝑋 ∈ 𝑉 ↔ ∃𝑥 ∈ {0, 1}∃𝑦 ∈ 𝐼 𝑋 = ⟨𝑥, 𝑦⟩))
Theorem	gpgvtxel2 49351	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 49352*	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 49353*	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 49354*	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 49355	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 49356	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 49357	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 49358	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 49359*	Lemma for gpgusgra 49360. (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 49360	The generalized Petersen graph GPG(N,K) is a simple graph. (Contributed by AV, 27-Aug-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (𝑁 gPetersenGr 𝐾) ∈ USGraph)
Theorem	gpgprismgrusgra 49361	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 49362	The order of the generalized Petersen graph GPG(N,K). (Contributed by AV, 29-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (♯‘(Vtx‘(𝑁 gPetersenGr 𝐾))) = (2 · 𝑁))
Theorem	gpg5order 49363	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 49364	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 49365	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 49366	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 49367	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 49368	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 49369	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 49370	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 49371	Lemma 1 for gpg5nbgrvtx03star 49383. (Contributed by AV, 5-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑊) → {⟨0, ((𝑋 + 1) mod 𝑁)⟩, ⟨1, 𝑋⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx03starlem2 49372	Lemma 2 for gpg5nbgrvtx03star 49383. (Contributed by AV, 6-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ ℤ) → {⟨0, ((𝑋 + 1) mod 𝑁)⟩, ⟨0, ((𝑋 − 1) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx03starlem3 49373	Lemma 3 for gpg5nbgrvtx03star 49383. (Contributed by AV, 5-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑊) → {⟨1, 𝑋⟩, ⟨0, ((𝑋 − 1) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem1 49374	Lemma 1 for gpg5nbgr3star 49384. (Contributed by AV, 7-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑊) → {⟨1, ((𝑋 + 𝐾) mod 𝑁)⟩, ⟨0, 𝑋⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem2 49375	Lemma 2 for gpg5nbgr3star 49384. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ ℤ) → {⟨1, ((𝑋 + 𝐾) mod 𝑁)⟩, ⟨1, ((𝑋 − 𝐾) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem3 49376	Lemma 3 for gpg5nbgr3star 49384. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑊) → {⟨0, 𝑋⟩, ⟨1, ((𝑋 − 𝐾) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpgnbgrvtx0 49377	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 49378	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 49379	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 49380	In a generalized Petersen graph 𝐺, every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025.) The proof of gpg3nbgrvtx0 49379 can be shortened using modmknepk 48643, but then theorem 2ltceilhalf 48607 is required which is based on an "example" ex-ceil 31079. 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 49381	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 49382	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 49385), i.e., every vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → (♯‘𝑈) = 3)
Theorem	gpg5nbgrvtx03star 49383*	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 49384*	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 49392. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → ((♯‘𝑈) = 3 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸))
Theorem	gpgvtxdg3 49385	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 49386	Lemma 1 for gpg3kgrtriex 49392. (Contributed by AV, 1-Oct-2025.)
⊢ (𝐾 ∈ ℕ → 𝐾 < (⌈‘((3 · 𝐾) / 2)))
Theorem	gpg3kgrtriexlem2 49387	Lemma 2 for gpg3kgrtriex 49392. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → ( -𝐾 mod 𝑁) = (((𝐾 mod 𝑁) + 𝐾) mod 𝑁))
Theorem	gpg3kgrtriexlem3 49388	Lemma 3 for gpg3kgrtriex 49392. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ (ℤ≥‘3))
Theorem	gpg3kgrtriexlem4 49389	Lemma 4 for gpg3kgrtriex 49392. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ (1..^(⌈‘(𝑁 / 2))))
Theorem	gpg3kgrtriexlem5 49390	Lemma 5 for gpg3kgrtriex 49392. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (𝐾 mod 𝑁) ≠ ( -𝐾 mod 𝑁))
Theorem	gpg3kgrtriexlem6 49391	Lemma 6 for gpg3kgrtriex 49392: 𝐸 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 49392*	All generalized Petersen graphs G(N,K) with 𝑁 = 3 · 𝐾 contain triangles. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺))
Theorem	gpg5gricstgr3 49393	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 49394	Lemma for theorems about Petersen graphs. (Contributed by AV, 10-Nov-2025.)
⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
Theorem	pgjsgr 49395	A Petersen graph is a simple graph. (Contributed by AV, 10-Nov-2025.)
⊢ (5 gPetersenGr 2) ∈ USGraph
Theorem	gpg5grlim 49396	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 49397	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 49398	Lemma 1 for gpgprismgr4cycl0 49409: 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 49399	Lemma 2 for gpgprismgr4cycl0 49409: 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 49400*	Lemma 3 for gpgprismgr4cycl0 49409. (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 𝑁)⟩})))