P. 484 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48301-48400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gpgorder 48301	The order of the generalized Petersen graph GPG(N,K). (Contributed by AV, 29-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (♯‘(Vtx‘(𝑁 gPetersenGr 𝐾))) = (2 · 𝑁))
Theorem	gpg5order 48302	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 48303	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 48304	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 48305	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 48306	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 48307	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 48308	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 48309	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 48310	Lemma 1 for gpg5nbgrvtx03star 48322. (Contributed by AV, 5-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑊) → {⟨0, ((𝑋 + 1) mod 𝑁)⟩, ⟨1, 𝑋⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx03starlem2 48311	Lemma 2 for gpg5nbgrvtx03star 48322. (Contributed by AV, 6-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ ℤ) → {⟨0, ((𝑋 + 1) mod 𝑁)⟩, ⟨0, ((𝑋 − 1) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx03starlem3 48312	Lemma 3 for gpg5nbgrvtx03star 48322. (Contributed by AV, 5-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑊) → {⟨1, 𝑋⟩, ⟨0, ((𝑋 − 1) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem1 48313	Lemma 1 for gpg5nbgr3star 48323. (Contributed by AV, 7-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑊) → {⟨1, ((𝑋 + 𝐾) mod 𝑁)⟩, ⟨0, 𝑋⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem2 48314	Lemma 2 for gpg5nbgr3star 48323. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ ℤ) → {⟨1, ((𝑋 + 𝐾) mod 𝑁)⟩, ⟨1, ((𝑋 − 𝐾) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpg5nbgrvtx13starlem3 48315	Lemma 3 for gpg5nbgr3star 48323. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 = 5 ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑊) → {⟨0, 𝑋⟩, ⟨1, ((𝑋 − 𝐾) mod 𝑁)⟩} ∉ 𝐸)
Theorem	gpgnbgrvtx0 48316	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 48317	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 48318	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 48319	In a generalized Petersen graph 𝐺, every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025.) The proof of gpg3nbgrvtx0 48318 can be shortened using modmknepk 47604, but then theorem 2ltceilhalf 47570 is required which is based on an "example" ex-ceil 30523. 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 48320	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 48321	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 48324), i.e., every vertex has exactly three (different) neighbors. (Contributed by AV, 3-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → (♯‘𝑈) = 3)
Theorem	gpg5nbgrvtx03star 48322*	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 48323*	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 48331. (Contributed by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 = 5 ∧ 𝐾 ∈ 𝐽 ∧ 𝑋 ∈ 𝑉) → ((♯‘𝑈) = 3 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸))
Theorem	gpgvtxdg3 48324	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 48325	Lemma 1 for gpg3kgrtriex 48331. (Contributed by AV, 1-Oct-2025.)
⊢ (𝐾 ∈ ℕ → 𝐾 < (⌈‘((3 · 𝐾) / 2)))
Theorem	gpg3kgrtriexlem2 48326	Lemma 2 for gpg3kgrtriex 48331. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (-𝐾 mod 𝑁) = (((𝐾 mod 𝑁) + 𝐾) mod 𝑁))
Theorem	gpg3kgrtriexlem3 48327	Lemma 3 for gpg3kgrtriex 48331. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ (ℤ≥‘3))
Theorem	gpg3kgrtriexlem4 48328	Lemma 4 for gpg3kgrtriex 48331. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ (1..^(⌈‘(𝑁 / 2))))
Theorem	gpg3kgrtriexlem5 48329	Lemma 5 for gpg3kgrtriex 48331. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → (𝐾 mod 𝑁) ≠ (-𝐾 mod 𝑁))
Theorem	gpg3kgrtriexlem6 48330	Lemma 6 for gpg3kgrtriex 48331: 𝐸 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 48331*	All generalized Petersen graphs G(N,K) with 𝑁 = 3 · 𝐾 contain triangles. (Contributed by AV, 1-Oct-2025.)
⊢ 𝑁 = (3 · 𝐾)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    ⇒   ⊢ (𝐾 ∈ ℕ → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺))
Theorem	gpg5gricstgr3 48332	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 48333	Lemma for theorems about Petersen graphs. (Contributed by AV, 10-Nov-2025.)
⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
Theorem	pgjsgr 48334	A Petersen graph is a simple graph. (Contributed by AV, 10-Nov-2025.)
⊢ (5 gPetersenGr 2) ∈ USGraph
Theorem	gpg5grlim 48335	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 48336	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 48337	Lemma 1 for gpgprismgr4cycl0 48348: 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 48338	Lemma 2 for gpgprismgr4cycl0 48348: 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 48339*	Lemma 3 for gpgprismgr4cycl0 48348. (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 48340	Lemma 4 for gpgprismgr4cycl0 48348: the cycle ⟨𝑃, 𝐹⟩ consists of 5 vertices (the first and the last vertex are identical, see gpgprismgr4cycllem6 48342. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ (♯‘𝑃) = 5
Theorem	gpgprismgr4cycllem5 48341	Lemma 5 for gpgprismgr4cycl0 48348. (Contributed by AV, 1-Nov-2025.)
⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩    ⇒   ⊢ 𝑃 ∈ Word V
Theorem	gpgprismgr4cycllem6 48342	Lemma 6 for gpgprismgr4cycl0 48348: 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 48343	Lemma 7 for gpgprismgr4cycl0 48348: 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 48344	Lemma 8 for gpgprismgr4cycl0 48348. (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 48345	Lemma 9 for gpgprismgr4cycl0 48348. (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 48346	Lemma 10 for gpgprismgr4cycl0 48348. (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 48347	Lemma 11 for gpgprismgr4cycl0 48348. (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 48348	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 48349*	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 48350	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 48351	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 48352	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 48353	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 48354	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 48355*	Lemma 1 for pgnbgreunbgr 48367. (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 48356*	Lemma 1 for pgnbgreunbgrlem2 48359. (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 48357*	Lemma 2 for pgnbgreunbgrlem2 48359. (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 48358*	Lemma 3 for pgnbgreunbgrlem2 48359. (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 48359*	Lemma 2 for pgnbgreunbgr 48367. 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 48360	Lemma 3 for pgnbgreunbgr 48367. (Contributed by AV, 18-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿) ∧ 𝑏 ∈ (0..^5)) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ∧ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨0, 𝑏⟩))
Theorem	pgnbgreunbgrlem4 48361*	Lemma 4 for pgnbgreunbgr 48367. (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 48362*	Lemma 1 for pgnbgreunbgrlem5 48365. (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 48363*	Lemma 2 for pgnbgreunbgrlem5 48365. (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 48364*	Lemma 3 for pgnbgreunbgrlem5 48365. (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 48365*	Lemma 5 for pgnbgreunbgr 48367. 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 48366	Lemma 6 for pgnbgreunbgr 48367. (Contributed by AV, 20-Nov-2025.)
⊢ 𝐺 = (5 gPetersenGr 2)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ (((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿) ∧ 𝑏 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
Theorem	pgnbgreunbgr 48367*	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 48368	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 48369	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 48370	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 48371*	There are two different locally isomorphic graphs which are not isomorphic. (Contributed by AV, 23-Nov-2025.)
⊢ ∃𝑔∃ℎ(𝑔 ≃𝑙𝑔𝑟 ℎ ∧ ¬ 𝑔 ≃𝑔𝑟 ℎ)
Theorem	gpg5edgnedg 48372	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 48373*	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 48372). This theorem proves that the analogon (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ 𝐾 ∈ 𝐼)) → (𝐹 “ 𝐾) ∈ 𝐸) of grimedgi 48178 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 48374*	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 48375	Extend class notation with walks (of a pseudograph).
class UPWalks
Definition	df-upwlks 48376*	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 48377*	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 48378*	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 48379*	Generalization of isupwlk 48378: 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 48380	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 48381	A simple walk is a walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 27-Feb-2021.)
⊢ (𝐹(UPWalks‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	upgrwlkupwlk 48382	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 48383	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 48384*	Alternate proof of upgriswlk 29714 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 48385	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 48386*	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 48396. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ⊆ (𝑊 × 𝑃))
Theorem	uspgrsprfv 48387*	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 48393. (Contributed by AV, 24-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑋 ∈ 𝐺 → (𝐹‘𝑋) = (2nd ‘𝑋))
Theorem	uspgrsprf 48388*	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 48389*	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 48390*	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 48391*	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 48396. (Contributed by AV, 25-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝐹 = (𝑔 ∈ 𝐺 ↦ (2nd ‘𝑔))    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝐺–1-1-onto→𝑃)
Theorem	uspgrex 48392*	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 48393*	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 48394*	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 48395*	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 48396. (Contributed by AV, 27-Nov-2021.)
⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ (𝑣 = 𝑉 ∧ ∃𝑞 ∈ USPGraph ((Vtx‘𝑞) = 𝑣 ∧ (Edg‘𝑞) = 𝑒))}    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑅)
Theorem	uspgrbisymrel 48396*	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 48392) 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 48397*	Alternate proof of uspgrbisymrel 48396 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 48398	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 6874. (Contributed by AV, 27-Jan-2020.)
⊢ ((𝐴𝐹𝐵) ≠ ∅ → (⟨𝐴, 𝐵⟩ ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {⟨𝐴, 𝐵⟩})))
Theorem	xpsnopab 48399*	A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020.)
⊢ ({𝑋} × 𝐶) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑋 ∧ 𝑏 ∈ 𝐶)}
Theorem	xpiun 48400*	A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.)
⊢ (𝐵 × 𝐶) = ∪ 𝑥 ∈ 𝐵 {⟨𝑎, 𝑏⟩ ∣ (𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶)}