P. 492 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49101-49200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gpg5nbgr3star 49101*	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 49109. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → ((♯‘𝑈) = 3 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸))
Theorem	gpgvtxdg3 49102	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 49103	Lemma 1 for gpg3kgrtriex 49109. (Contributed by AV, 1-Oct-2025.)
⊢ (𝐾 ∈ ℕ → 𝐾 < (⌈‘((3 · 𝐾) / 2)))
Theorem	gpg3kgrtriexlem2 49104	Lemma 2 for gpg3kgrtriex 49109. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (-𝐾 mod 𝑁) = (((𝐾 mod 𝑁) + 𝐾) mod 𝑁))
Theorem	gpg3kgrtriexlem3 49105	Lemma 3 for gpg3kgrtriex 49109. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ (ℤ≥‘3))
Theorem	gpg3kgrtriexlem4 49106	Lemma 4 for gpg3kgrtriex 49109. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ (1..^(⌈‘(𝑁 / 2))))
Theorem	gpg3kgrtriexlem5 49107	Lemma 5 for gpg3kgrtriex 49109. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (𝐾 mod 𝑁) ≠ (-𝐾 mod 𝑁))
Theorem	gpg3kgrtriexlem6 49108	Lemma 6 for gpg3kgrtriex 49109: 𝐸 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 49109*	All generalized Petersen graphs G(N,K) with 𝑁 = 3 · 𝐾 contain triangles. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺))
Theorem	gpg5gricstgr3 49110	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 49111	Lemma for theorems about Petersen graphs. (Contributed by AV, 10-Nov-2025.)
⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
Theorem	pgjsgr 49112	A Petersen graph is a simple graph. (Contributed by AV, 10-Nov-2025.)
⊢ (5 gPetersenGr 2) ∈ USGraph
Theorem	gpg5grlim 49113	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 49114	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 49115	Lemma 1 for gpgprismgr4cycl0 49126: 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 49116	Lemma 2 for gpgprismgr4cycl0 49126: 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 49117*	Lemma 3 for gpgprismgr4cycl0 49126. (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 49118	Lemma 4 for gpgprismgr4cycl0 49126: the cycle ⟨𝑃, 𝐹⟩ consists of 5 vertices (the first and the last vertex are identical, see gpgprismgr4cycllem6 49120. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ (♯‘𝑃) = 5
Theorem	gpgprismgr4cycllem5 49119	Lemma 5 for gpgprismgr4cycl0 49126. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ 𝑃 ∈ Word V
Theorem	gpgprismgr4cycllem6 49120	Lemma 6 for gpgprismgr4cycl0 49126: 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 49121	Lemma 7 for gpgprismgr4cycl0 49126: 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 49122	Lemma 8 for gpgprismgr4cycl0 49126. (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 49123	Lemma 9 for gpgprismgr4cycl0 49126. (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 49124	Lemma 10 for gpgprismgr4cycl0 49126. (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 49125	Lemma 11 for gpgprismgr4cycl0 49126. (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 49126	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 49127*	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 49128	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 49129	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 49130	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 49131	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 49132	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 49133*	Lemma 1 for pgnbgreunbgr 49145. (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 49134*	Lemma 1 for pgnbgreunbgrlem2 49137. (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 49135*	Lemma 2 for pgnbgreunbgrlem2 49137. (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 49136*	Lemma 3 for pgnbgreunbgrlem2 49137. (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 49137*	Lemma 2 for pgnbgreunbgr 49145. 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 49138	Lemma 3 for pgnbgreunbgr 49145. (Contributed by AV, 18-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿) ∧ 𝑏 ∈ (0..^5)) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ∧ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨0, 𝑏⟩))
Theorem	pgnbgreunbgrlem4 49139*	Lemma 4 for pgnbgreunbgr 49145. (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, 𝑏⟩)))))
Theorem	pgnbgreunbgrlem5lem1 49140*	Lemma 1 for pgnbgreunbgrlem5 49143. (Contributed by AV, 21-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
Theorem	pgnbgreunbgrlem5lem2 49141*	Lemma 2 for pgnbgreunbgrlem5 49143. (Contributed by AV, 20-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
Theorem	pgnbgreunbgrlem5lem3 49142*	Lemma 3 for pgnbgreunbgrlem5 49143. (Contributed by AV, 20-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
Theorem	pgnbgreunbgrlem5 49143*	Lemma 5 for pgnbgreunbgr 49145. Impossible cases. (Contributed by AV, 21-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))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))))
Theorem	pgnbgreunbgrlem6 49144	Lemma 6 for pgnbgreunbgr 49145. (Contributed by AV, 20-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿) ∧ 𝑏 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
Theorem	pgnbgreunbgr 49145*	In a Petersen graph, two different neighbors of a vertex have exactly one common neighbor, which is the vertex itself. (Contributed by AV, 9-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿) → ∃!𝑥 ∈ 𝑉 {{𝐾, 𝑥}, {𝑥, 𝐿}} ⊆ 𝐸)
Theorem	pgn4cyclex 49146	A cycle in a Petersen graph G(5,2) does not have length 4. (Contributed by AV, 9-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    ⇒   ⊢ (𝐹(Cycles‘𝐺)𝑃 → (♯‘𝐹) ≠ 4)
Theorem	pg4cyclnex 49147	In the Petersen graph G(5,2), there is no cycle of length 4. (Contributed by AV, 22-Nov-2025.)
⊢ ¬ ∃𝑝∃𝑓(𝑓(Cycles‘(5 gPetersenGr 2))𝑝 ∧ (♯‘𝑓) = 4)
Theorem	gpg5ngric 49148	The two generalized Petersen graphs G(5,K) of order 10, which are the Petersen graph G(5,2) and the 5-prism G(5,1), are not isomorphic. (Contributed by AV, 22-Nov-2025.)
⊢ ¬ (5 gPetersenGr 1) ≃𝑔𝑟 (5 gPetersenGr 2)
Theorem	lgricngricex 49149*	There are two different locally isomorphic graphs which are not isomorphic. (Contributed by AV, 23-Nov-2025.)
⊢ ∃𝑔∃ℎ(𝑔 ≃𝑙𝑔𝑟 ℎ ∧ ¬ 𝑔 ≃𝑔𝑟 ℎ)
Theorem	gpg5edgnedg 49150	Two consecutive (according to the numbering) inside vertices of the Petersen graph G(5,2) are not connected by an edge, but are connected by an edge in a 5-prism G(5,1). (Contributed by AV, 29-Dec-2025.)
⊢ ({⟨1, 0⟩, ⟨1, 1⟩} ∈ (Edg‘(5 gPetersenGr 1)) ∧ {⟨1, 0⟩, ⟨1, 1⟩} ∉ (Edg‘(5 gPetersenGr 2)))
Theorem	grlimedgnedg 49151*	In general, the image of an edge of a graph by a local isomprphism is not an edge of the other graph, proven by an example (see gpg5edgnedg 49150). This theorem proves that the analogon (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ 𝐾 ∈ 𝐼)) → (𝐹 “ 𝐾) ∈ 𝐸) of grimedgi 48956 for ordinarily isomorphic graphs does not hold in general. (Contributed by AV, 30-Dec-2025.)
⊢ ∃𝑔 ∈ USGraph ∃ℎ ∈ USGraph ∃𝑓 ∈ (𝑔 GraphLocIso ℎ)∃𝑎 ∈ (Vtx‘𝑔)∃𝑏 ∈ (Vtx‘𝑔)({𝑎, 𝑏} ∈ (Edg‘𝑔) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ))
21.50.15.9  Loop-free graphs - extension
Theorem	1hegrlfgr 49152*	A graph 𝐺 with one hyperedge joining at least two vertices is a loop-free graph. (Contributed by AV, 23-Feb-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸)    ⇒   ⊢ (𝜑 → (iEdg‘𝐺):{𝐴}⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})
21.50.15.10  Walks - extension
Syntax	cupwlks 49153	Extend class notation with walks (of a pseudograph).
class UPWalks
Definition	df-upwlks 49154*	Define the set of all walks (in a pseudograph), called "simple walks" in the following. According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A walk of length k in a graph is an alternating sequence of vertices and edges, v0 , e0 , v1 , e1 , v2 , ... , v(k-1) , e(k-1) , v(k) which begins and ends with vertices. If the graph is undirected, then the endpoints of e(i) are v(i) and v(i+1)." According to Bollobas: " A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. Therefore, a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Although this definition is also applicable for arbitrary hypergraphs, it allows only walks consisting of not proper hyperedges (i.e. edges connecting at most two vertices). Therefore, it should be used for pseudographs only. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})
Theorem	upwlksfval 49155*	The set of simple walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (UPWalks‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})
Theorem	isupwlk 49156*	Properties of a pair of functions to be a simple walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(UPWalks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
Theorem	isupwlkg 49157*	Generalization of isupwlk 49156: Conditions for two classes to represent a simple walk. (Contributed by AV, 5-Nov-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐹(UPWalks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
Theorem	upwlkbprop 49158	Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 29-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(UPWalks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
Theorem	upwlkwlk 49159	A simple walk is a walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 27-Feb-2021.)
⊢ (𝐹(UPWalks‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	upgrwlkupwlk 49160	In a pseudograph, a walk is a simple walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 2-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → 𝐹(UPWalks‘𝐺)𝑃)
Theorem	upgrwlkupwlkb 49161	In a pseudograph, the definitions for a walk and a simple walk are equivalent. (Contributed by AV, 30-Dec-2020.)
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ 𝐹(UPWalks‘𝐺)𝑃))
Theorem	upgrisupwlkALT 49162*	Alternate proof of upgriswlk 30155 using the definition of UPGraph and related theorems. (Contributed by AV, 2-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
21.50.15.11  Edges of graphs expressed as sets of unordered pairs
Theorem	upgredgssspr 49163	The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 24-Nov-2021.)
⊢ (𝐺 ∈ UPGraph → (Edg‘𝐺) ⊆ (Pairs‘(Vtx‘𝐺)))
Theorem	uspgropssxp 49164*	The set 𝐺 of "simple pseudographs" for a fixed set 𝑉 of vertices is a subset of a Cartesian product. For more details about the class 𝐺 of all "simple pseudographs" see comments on uspgrbisymrel 49174. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ⊆ (𝑊 × 𝑃))
Theorem	uspgrsprfv 49165*	The value of the function 𝐹 which maps a "simple pseudograph" for a fixed set 𝑉 of vertices to the set of edges (i.e. range of the edge function) of the graph. Solely for 𝐺 as defined here, the function 𝐹 is a bijection between the "simple pseudographs" and the subsets of the set of pairs 𝑃 over the fixed set 𝑉 of vertices, see uspgrbispr 49171. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑋 ∈ 𝐺 → (𝐹‘𝑋) = (2nd ‘𝑋))
Theorem	uspgrsprf 49166*	The mapping 𝐹 is a function from the "simple pseudographs" with a fixed set of vertices 𝑉 into the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ 𝐹:𝐺⟶𝑃
Theorem	uspgrsprf1 49167*	The mapping 𝐹 is a one-to-one function from the "simple pseudographs" with a fixed set of vertices 𝑉 into the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 25-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ 𝐹:𝐺–1-1→𝑃
Theorem	uspgrsprfo 49168*	The mapping 𝐹 is a function from the "simple pseudographs" with a fixed set of vertices 𝑉 onto the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 25-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝐺–onto→𝑃)
Theorem	uspgrsprf1o 49169*	The mapping 𝐹 is a bijection between the "simple pseudographs" with a fixed set of vertices 𝑉 and the subsets of the set of pairs over the set 𝑉. See also the comments on uspgrbisymrel 49174. (Contributed by AV, 25-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝐺–1-1-onto→𝑃)
Theorem	uspgrex 49170*	The class 𝐺 of all "simple pseudographs" with a fixed set of vertices 𝑉 is a set. (Contributed by AV, 26-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ∈ V)
Theorem	uspgrbispr 49171*	There is a bijection between the "simple pseudographs" with a fixed set of vertices 𝑉 and the subsets of the set of pairs over the set 𝑉. (Contributed by AV, 26-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ∃𝑓 𝑓:𝐺–1-1-onto→𝑃)
Theorem	uspgrspren 49172*	The set 𝐺 of the "simple pseudographs" with a fixed set of vertices 𝑉 and the class 𝑃 of subsets of the set of pairs over the fixed set 𝑉 are equinumerous. (Contributed by AV, 27-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑃)
Theorem	uspgrymrelen 49173*	The set 𝐺 of the "simple pseudographs" with a fixed set of vertices 𝑉 and the class 𝑅 of the symmetric relations on the fixed set 𝑉 are equinumerous. For more details about the class 𝐺 of all "simple pseudographs" see comments on uspgrbisymrel 49174. (Contributed by AV, 27-Nov-2021.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑅)
Theorem	uspgrbisymrel 49174*	There is a bijection between the "simple pseudographs" for a fixed set 𝑉 of vertices and the class 𝑅 of the symmetric relations on the fixed set 𝑉. The simple pseudographs, which are graphs without hyper- or multiedges, but which may contain loops, are expressed as ordered pairs of the vertices and the edges (as proper or improper unordered pairs of vertices, not as indexed edges!) in this theorem. That class 𝐺 of such simple pseudographs is a set (if 𝑉 is a set, see uspgrex 49170) of equivalence classes of graphs abstracting from the index sets of their edge functions. Solely for this abstraction, there is a bijection between the "simple pseudographs" as members of 𝐺 and the symmetric relations 𝑅 on the fixed set 𝑉 of vertices. This theorem would not hold for 𝐺 = {𝑔 ∈ USPGraph ∣ (Vtx‘𝑔) = 𝑉} and even not for 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ⟨𝑣, 𝑒⟩ ∈ USPGraph)}, because these are much bigger classes. (Proposed by Gerard Lang, 16-Nov-2021.) (Contributed by AV, 27-Nov-2021.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ∃𝑓 𝑓:𝐺–1-1-onto→𝑅)
Theorem	uspgrbisymrelALT 49175*	Alternate proof of uspgrbisymrel 49174 not using the definition of equinumerosity. (Contributed by AV, 26-Nov-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ∃𝑓 𝑓:𝐺–1-1-onto→𝑅)
21.50.16  Monoids (extension)
21.50.16.1  Auxiliary theorems
Theorem	ovn0dmfun 49176	If a class operation value for two operands is not the empty set, then the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 6913. (Contributed by AV, 27-Jan-2020.)
⊢ ((𝐴𝐹𝐵) ≠ ∅ → (⟨𝐴, 𝐵⟩ ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {⟨𝐴, 𝐵⟩})))
Theorem	xpsnopab 49177*	A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020.)
⊢ ({𝑋} × 𝐶) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶)}
Theorem	xpiun 49178*	A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.)
⊢ (𝐵 × 𝐶) = ∪ 𝑥 ∈ 𝐵 {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶)}
Theorem	fnxpdmdm 49179	The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020.)
⊢ (𝐹 Fn (𝐴 × 𝐴) → dom dom 𝐹 = 𝐴)
Theorem	cnfldsrngbas 49180	The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ⊆ ℂ → 𝑆 = (Base‘𝑅))
Theorem	cnfldsrngadd 49181	The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ 𝑉 → + = (+g‘𝑅))
Theorem	cnfldsrngmul 49182	The ring multiplication operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ 𝑉 → · = (.r‘𝑅))
21.50.16.2  Magmas, Semigroups and Monoids (extension)
Theorem	plusfreseq 49183	If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily a magma), the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ⨣ = (+𝑓‘𝑀)    ⇒   ⊢ (∅ ∉ ran ⨣ → ( + ↾ (𝐵 × 𝐵)) = ⨣ )
Theorem	mgmplusfreseq 49184	If the empty set is not contained in the base set of a magma, the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ⨣ = (+𝑓‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mgm ∧ ∅ ∉ 𝐵) → ( + ↾ (𝐵 × 𝐵)) = ⨣ )
Theorem	0mgm 49185	A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020.)
⊢ (Base‘𝑀) = ∅    ⇒   ⊢ (𝑀 ∈ 𝑉 → 𝑀 ∈ Mgm)
21.50.16.3  Examples and counterexamples for magmas, semigroups and monoids (extension)
Theorem	opmpoismgm 49186*	A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑀 ∈ Mgm)
Theorem	copissgrp 49187*	A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑀 ∈ Smgrp)
Theorem	copisnmnd 49188*	A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 1 < (♯‘𝐵))    ⇒   ⊢ (𝜑 → 𝑀 ∉ Mnd)
Theorem	0nodd 49189*	0 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 0 ∉ 𝑂
Theorem	1odd 49190*	1 is an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 1 ∈ 𝑂
Theorem	2nodd 49191*	2 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 2 ∉ 𝑂
Theorem	oddibas 49192*	Lemma 1 for oddinmgm 49194: The base set of M is the set of all odd integers. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    &   ⊢ 𝑀 = (ℂfld ↾s 𝑂)    ⇒   ⊢ 𝑂 = (Base‘𝑀)
Theorem	oddiadd 49193*	Lemma 2 for oddinmgm 49194: The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    &   ⊢ 𝑀 = (ℂfld ↾s 𝑂)    ⇒   ⊢ + = (+g‘𝑀)
Theorem	oddinmgm 49194*	The structure of all odd integers together with the addition of complex numbers is not a magma. Remark: the structure of the complementary subset of the set of integers, the even integers, is a magma, actually an abelian group, see 2zrngaabl 49269, and even a non-unital ring, see 2zrng 49260. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    &   ⊢ 𝑀 = (ℂfld ↾s 𝑂)    ⇒   ⊢ 𝑀 ∉ Mgm
Theorem	nnsgrpmgm 49195	The structure of positive integers together with the addition of complex numbers is a magma. (Contributed by AV, 4-Feb-2020.)
⊢ 𝑀 = (ℂfld ↾s ℕ)    ⇒   ⊢ 𝑀 ∈ Mgm
Theorem	nnsgrp 49196	The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.)
⊢ 𝑀 = (ℂfld ↾s ℕ)    ⇒   ⊢ 𝑀 ∈ Smgrp
Theorem	nnsgrpnmnd 49197	The structure of positive integers together with the addition of complex numbers is not a monoid. (Contributed by AV, 4-Feb-2020.)
⊢ 𝑀 = (ℂfld ↾s ℕ)    ⇒   ⊢ 𝑀 ∉ Mnd
Theorem	nn0mnd 49198	The set of nonnegative integers under (complex) addition is a monoid. Example in [Lang] p. 6. Remark: 𝑀 could have also been written as (ℂfld ↾s ℕ0). (Contributed by AV, 27-Dec-2023.)
⊢ 𝑀 = {⟨(Base‘ndx), ℕ0⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ 𝑀 ∈ Mnd
21.50.16.4  Group sum operation (extension 1)
Theorem	gsumsplit2f 49199*	Split a group sum into two parts. (Contributed by AV, 4-Sep-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 )    &   ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)    &   ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)) + (𝐺 Σg (𝑘 ∈ 𝐷 ↦ 𝑋))))
Theorem	gsumdifsndf 49200*	Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.)
⊢ Ⅎ𝑘𝑌    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp (0g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ (𝐴 ∖ {𝑀}) ↦ 𝑋)) + 𝑌))