P. 483 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48201-48300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pglem 48201	Lemma for theorems about Petersen graphs. (Contributed by AV, 10-Nov-2025.)
⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
Theorem	pgjsgr 48202	A Petersen graph is a simple graph. (Contributed by AV, 10-Nov-2025.)
⊢ (5 gPetersenGr 2) ∈ USGraph
Theorem	gpg5grlim 48203	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 48204	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 48205	Lemma 1 for gpgprismgr4cycl0 48216: 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 48206	Lemma 2 for gpgprismgr4cycl0 48216: 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 48207*	Lemma 3 for gpgprismgr4cycl0 48216. (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 48208	Lemma 4 for gpgprismgr4cycl0 48216: the cycle ⟨𝑃, 𝐹⟩ consists of 5 vertices (the first and the last vertex are identical, see gpgprismgr4cycllem6 48210. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ (♯‘𝑃) = 5
Theorem	gpgprismgr4cycllem5 48209	Lemma 5 for gpgprismgr4cycl0 48216. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ 𝑃 ∈ Word V
Theorem	gpgprismgr4cycllem6 48210	Lemma 6 for gpgprismgr4cycl0 48216: 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 48211	Lemma 7 for gpgprismgr4cycl0 48216: 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 48212	Lemma 8 for gpgprismgr4cycl0 48216. (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 48213	Lemma 9 for gpgprismgr4cycl0 48216. (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 48214	Lemma 10 for gpgprismgr4cycl0 48216. (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 48215	Lemma 11 for gpgprismgr4cycl0 48216. (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 48216	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 48217*	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 48218	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 48219	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 48220	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 48221	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 48222	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 48223*	Lemma 1 for pgnbgreunbgr 48235. (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 48224*	Lemma 1 for pgnbgreunbgrlem2 48227. (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 48225*	Lemma 2 for pgnbgreunbgrlem2 48227. (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 48226*	Lemma 3 for pgnbgreunbgrlem2 48227. (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 48227*	Lemma 2 for pgnbgreunbgr 48235. 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 48228	Lemma 3 for pgnbgreunbgr 48235. (Contributed by AV, 18-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿) ∧ 𝑏 ∈ (0..^5)) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ∧ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨0, 𝑏⟩))
Theorem	pgnbgreunbgrlem4 48229*	Lemma 4 for pgnbgreunbgr 48235. (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 48230*	Lemma 1 for pgnbgreunbgrlem5 48233. (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 48231*	Lemma 2 for pgnbgreunbgrlem5 48233. (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 48232*	Lemma 3 for pgnbgreunbgrlem5 48233. (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 48233*	Lemma 5 for pgnbgreunbgr 48235. 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 48234	Lemma 6 for pgnbgreunbgr 48235. (Contributed by AV, 20-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿) ∧ 𝑏 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
Theorem	pgnbgreunbgr 48235*	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 48236	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 48237	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 48238	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 48239*	There are two different locally isomorphic graphs which are not isomorphic. (Contributed by AV, 23-Nov-2025.)
⊢ ∃𝑔∃ℎ(𝑔 ≃𝑙𝑔𝑟 ℎ ∧ ¬ 𝑔 ≃𝑔𝑟 ℎ)
Theorem	gpg5edgnedg 48240	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 48241*	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 48240). This theorem proves that the analogon (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ 𝐾 ∈ 𝐼)) → (𝐹 “ 𝐾) ∈ 𝐸) of grimedgi 48046 for ordinarily isomorphic graphs does not hold in general. (Contributed by AV, 30-Dec-2025.)
⊢ ∃𝑔 ∈ USGraph ∃ℎ ∈ USGraph ∃𝑓 ∈ (𝑔 GraphLocIso ℎ)∃𝑎 ∈ (Vtx‘𝑔)∃𝑏 ∈ (Vtx‘𝑔)({𝑎, 𝑏} ∈ (Edg‘𝑔) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∉ (Edg‘ℎ))
21.48.15.9  Loop-free graphs - extension
Theorem	1hegrlfgr 48242*	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.48.15.10  Walks - extension
Syntax	cupwlks 48243	Extend class notation with walks (of a pseudograph).
class UPWalks
Definition	df-upwlks 48244*	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 48245*	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 48246*	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 48247*	Generalization of isupwlk 48246: 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 48248	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 48249	A simple walk is a walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 27-Feb-2021.)
⊢ (𝐹(UPWalks‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	upgrwlkupwlk 48250	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 48251	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 48252*	Alternate proof of upgriswlk 29619 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.48.15.11  Edges of graphs expressed as sets of unordered pairs
Theorem	upgredgssspr 48253	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 48254*	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 48264. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ⊆ (𝑊 × 𝑃))
Theorem	uspgrsprfv 48255*	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 48261. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑋 ∈ 𝐺 → (𝐹‘𝑋) = (2nd ‘𝑋))
Theorem	uspgrsprf 48256*	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 48257*	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 48258*	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 48259*	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 48264. (Contributed by AV, 25-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝐺–1-1-onto→𝑃)
Theorem	uspgrex 48260*	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 48261*	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 48262*	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 48263*	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 48264. (Contributed by AV, 27-Nov-2021.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑅)
Theorem	uspgrbisymrel 48264*	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 48260) 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 48265*	Alternate proof of uspgrbisymrel 48264 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.48.16  Monoids (extension)
21.48.16.1  Auxiliary theorems
Theorem	ovn0dmfun 48266	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 6862. (Contributed by AV, 27-Jan-2020.)
⊢ ((𝐴𝐹𝐵) ≠ ∅ → (⟨𝐴, 𝐵⟩ ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {⟨𝐴, 𝐵⟩})))
Theorem	xpsnopab 48267*	A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020.)
⊢ ({𝑋} × 𝐶) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶)}
Theorem	xpiun 48268*	A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.)
⊢ (𝐵 × 𝐶) = ∪ 𝑥 ∈ 𝐵 {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶)}
Theorem	ovn0ssdmfun 48269*	If a class' operation value for two operands is not the empty set, the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 6862. (Contributed by AV, 27-Jan-2020.)
⊢ (∀𝑎 ∈ 𝐷 ∀𝑏 ∈ 𝐸 (𝑎𝐹𝑏) ≠ ∅ → ((𝐷 × 𝐸) ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ (𝐷 × 𝐸))))
Theorem	fnxpdmdm 48270	The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020.)
⊢ (𝐹 Fn (𝐴 × 𝐴) → dom dom 𝐹 = 𝐴)
Theorem	cnfldsrngbas 48271	The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ⊆ ℂ → 𝑆 = (Base‘𝑅))
Theorem	cnfldsrngadd 48272	The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ 𝑉 → + = (+g‘𝑅))
Theorem	cnfldsrngmul 48273	The ring multiplication operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
⊢ 𝑅 = (ℂfld ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ 𝑉 → · = (.r‘𝑅))
21.48.16.2  Magmas, Semigroups and Monoids (extension)
Theorem	plusfreseq 48274	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 48275	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 48276	A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020.)
⊢ (Base‘𝑀) = ∅    ⇒   ⊢ (𝑀 ∈ 𝑉 → 𝑀 ∈ Mgm)
21.48.16.3  Examples and counterexamples for magmas, semigroups and monoids (extension)
Theorem	opmpoismgm 48277*	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 48278*	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 48279*	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 48280*	0 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 0 ∉ 𝑂
Theorem	1odd 48281*	1 is an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 1 ∈ 𝑂
Theorem	2nodd 48282*	2 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    ⇒   ⊢ 2 ∉ 𝑂
Theorem	oddibas 48283*	Lemma 1 for oddinmgm 48285: 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 48284*	Lemma 2 for oddinmgm 48285: 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 48285*	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 48360, and even a non-unital ring, see 2zrng 48351. (Contributed by AV, 3-Feb-2020.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = ((2 · 𝑥) + 1)}    &   ⊢ 𝑀 = (ℂfld ↾s 𝑂)    ⇒   ⊢ 𝑀 ∉ Mgm
Theorem	nnsgrpmgm 48286	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 48287	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 48288	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 48289	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.48.16.4  Group sum operation (extension 1)
Theorem	gsumsplit2f 48290*	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 48291*	Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.)
⊢ Ⅎ𝑘𝑌    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp (0g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌)    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ (𝐴 ∖ {𝑀}) ↦ 𝑋)) + 𝑌))
Theorem	gsumfsupp 48292	A group sum of a family can be restricted to the support of that family without changing its value, provided that that support is finite. This corresponds to the definition of an (infinite) product in [Lang] p. 5, last two formulas. (Contributed by AV, 27-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (𝐹 supp 0 )    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐼)) = (𝐺 Σg 𝐹))
21.48.17  Magmas and internal binary operations (alternate approach) With df-mpo 7351, binary operations are defined by a rule, and with df-ov 7349, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation 7349 (19-Jan-2020), "... a binary operation on a set 𝑆 is a mapping of the elements of the Cartesian product 𝑆 × 𝑆 to S: 𝑓:𝑆 × 𝑆⟶𝑆. Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, we call binary operations mapping the elements of the Cartesian product 𝑆 × 𝑆 internal binary operations, see df-intop 48309. If, in addition, the result is also contained in the set 𝑆, the operation is called closed internal binary operation, see df-clintop 48310. Therefore, a "binary operation on a set 𝑆 " according to Wikipedia is a "closed internal binary operation" in our terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations 48310 ). Taking a step back, we define "laws" applicable for "binary operations" (which even need not to be functions), according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7. These laws are used, on the one hand, to specialize internal binary operations (see df-clintop 48310 and df-assintop 48311), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obey these laws, are defined afterwards. Notice that in [BourbakiAlg1] p. 1, p. 4 and p. 7, these operations are called "laws" by themselves. In the following, an alternate definition df-cllaw 48296 for an internal binary operation is provided, which does not require function-ness, but only closure. Therefore, this definition could be used as binary operation (Slot 2) defined for a magma as extensible structure, see mgmplusgiopALT 48304, or for an alternate definition df-mgm2 48329 for a magma as extensible structure. Similar results are obtained for an associative operation (defining semigroups).
21.48.17.1  Laws for internal binary operations In this subsection, the "laws" applicable for "binary operations" according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7 are defined. These laws are called "internal laws" in [BourbakiAlg1] p. xxi.
Syntax	ccllaw 48293	Extend class notation for the closure law.
class clLaw
Syntax	casslaw 48294	Extend class notation for the associative law.
class assLaw
Syntax	ccomlaw 48295	Extend class notation for the commutative law.
class comLaw
Definition	df-cllaw 48296*	The closure law for binary operations, see definitions of laws A0. and M0. in section 1.1 of [Hall] p. 1, or definition 1 in [BourbakiAlg1] p. 1: the value of a binary operation applied to two operands of a given sets is an element of this set. By this definition, the closure law is expressed as binary relation: a binary operation is related to a set by clLaw if the closure law holds for this binary operation regarding this set. Note that the binary operation needs not to be a function. (Contributed by AV, 7-Jan-2020.)
⊢ clLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) ∈ 𝑚}
Definition	df-comlaw 48297*	The commutative law for binary operations, see definitions of laws A2. and M2. in section 1.1 of [Hall] p. 1, or definition 8 in [BourbakiAlg1] p. 7: the value of a binary operation applied to two operands equals the value of a binary operation applied to the two operands in reversed order. By this definition, the commutative law is expressed as binary relation: a binary operation is related to a set by comLaw if the commutative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by AV, 7-Jan-2020.)
⊢ comLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)}
Definition	df-asslaw 48298*	The associative law for binary operations, see definitions of laws A1. and M1. in section 1.1 of [Hall] p. 1, or definition 5 in [BourbakiAlg1] p. 4: the value of a binary operation applied the value of the binary operation applied to two operands and a third operand equals the value of the binary operation applied to the first operand and the value of the binary operation applied to the second and third operand. By this definition, the associative law is expressed as binary relation: a binary operation is related to a set by assLaw if the associative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.)
⊢ assLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 ∀𝑧 ∈ 𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
Theorem	iscllaw 48299*	The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.)
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ clLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) ∈ 𝑀))
Theorem	iscomlaw 48300*	The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.)
⊢ (( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊) → ( ⚬ comLaw 𝑀 ↔ ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (𝑥 ⚬ 𝑦) = (𝑦 ⚬ 𝑥)))