P. 493 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49201-49300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	stgrnbgr0 49201	All vertices of a star graph SN except the center are in the (open) neighborhood of the center. (Contributed by AV, 12-Sep-2025.)
⊢ 𝐺 = (StarGr‘𝑁)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐺 NeighbVtx 0) = (𝑉 ∖ {0}))
Theorem	stgrclnbgr0 49202	All vertices of a star graph SN are in the closed neighborhood of the center. (Contributed by AV, 12-Sep-2025.)
⊢ 𝐺 = (StarGr‘𝑁)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐺 ClNeighbVtx 0) = 𝑉)
Theorem	isubgr3stgrlem1 49203	Lemma 1 for isubgr3stgr 49212. (Contributed by AV, 16-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝐹 = (𝐻 ∪ {⟨𝑋, 𝑌⟩})    ⇒   ⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐹:𝐶–1-1-onto→(𝑅 ∪ {𝑌}))
Theorem	isubgr3stgrlem2 49204*	Lemma 2 for isubgr3stgr 49212. (Contributed by AV, 16-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}))
Theorem	isubgr3stgrlem3 49205*	Lemma 3 for isubgr3stgr 49212. (Contributed by AV, 17-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0))
Theorem	isubgr3stgrlem4 49206*	Lemma 4 for isubgr3stgr 49212. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐴 = 𝑋 ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧})
Theorem	isubgr3stgrlem5 49207*	Lemma 5 for isubgr3stgr 49212. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((𝐹:𝐶⟶𝑊 ∧ 𝑌 ∈ 𝐼) → (𝐻‘𝑌) = (𝐹 “ 𝑌))
Theorem	isubgr3stgrlem6 49208*	Lemma 6 for isubgr3stgr 49212. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼⟶(Edg‘(StarGr‘𝑁)))
Theorem	isubgr3stgrlem7 49209*	Lemma 7 for isubgr3stgr 49212. (Contributed by AV, 29-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝐽) ∈ 𝐼)
Theorem	isubgr3stgrlem8 49210*	Lemma 8 for isubgr3stgr 49212. (Contributed by AV, 29-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼–1-1-onto→(Edg‘(StarGr‘𝑁)))
Theorem	isubgr3stgrlem9 49211*	Lemma 9 for isubgr3stgr 49212. (Contributed by AV, 29-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐻:𝐼–1-1-onto→(Edg‘(StarGr‘𝑁)) ∧ ∀𝑒 ∈ 𝐼 (𝐹 “ 𝑒) = (𝐻‘𝑒)))
Theorem	isubgr3stgr 49212*	If a vertex of a simple graph has exactly 𝑁 (different) neighbors, and none of these neighbors are connected by an edge, then the (closed) neighborhood of this vertex induces a subgraph which is isomorphic to an 𝑁-star. (Contributed by AV, 29-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸) → (𝐺 ISubGr 𝐶) ≃𝑔𝑟 (StarGr‘𝑁)))
21.52.15.7  Local isomorphisms of graphs This section is about local isomorphisms of graphs, which are a generalization of isomorphisms of graphs, i.e., every isomorphism between two graphs is also a local isomorphism between these graphs, see uhgrimgrlim 49224. This definition is according to a chat in mathoverflow (https://mathoverflow.net/questions/491133/locally-isomorphic-graphs 49224): roughly speaking, it restricts the correspondence of two graphs to their neighborhoods. Additionally, a binary relation ≃𝑙𝑔𝑟 is defined (see df-grlic 49218) which is true for two graphs iff there is a local isomorphism between these graphs. Then these graphs are called "locally isomorphic". Therefore, this relation is also called "is locally isomorphic to" relation. As a main result of this section, it is shown that the "is locally isomorphic to" relation is an equivalence relation (for hypergraphs), see grlicer 49253. The names and symbols are chosen analogously to group isomorphisms GrpIso (see df-gim 19485) and graph isomorphisms GraphIso (see df-grim 49115) resp. isomorphism between groups ≃𝑔 (see df-gic 19486) and isomorphism between graphs ≃𝑔𝑟 (see df-gric 49118). As discussed in the above mentioned chat in mathoverflow, it is shown that there are local isomorphisms between two graphs which are not (ordinary) isomorphisms between these graphs. In other words, there are two different locally isomorphic graphs which are not isomorphic, see lgricngricex 49366. Such two graphs are the two generalized Petersen graphs G(5,K) of order 10 (see definition df-gpg 49278), which are the Petersen graph G(5,2) and the 5-prism G(5,1), see gpg5ngric 49365.
Syntax	cgrlim 49213	The class of graph local isomorphism sets.
class GraphLocIso
Syntax	cgrlic 49214	The class of the graph local isomorphism relation.
class ≃𝑙𝑔𝑟
Definition	df-grlim 49215*	A local isomorphism of graphs is a bijection between the sets of vertices of two graphs that preserves local adjacency, i.e. the subgraph induced by the closed neighborhood of a vertex of the first graph and the subgraph induced by the closed neighborhood of the associated vertex of the second graph are isomorphic. See the following chat in mathoverflow: https://mathoverflow.net/questions/491133/locally-isomorphic-graphs. (Contributed by AV, 27-Apr-2025.)
⊢ GraphLocIso = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))})
Theorem	grlimfn 49216	The graph local isomorphism function is a well-defined function. (Contributed by AV, 20-May-2025.)
⊢ GraphLocIso Fn (V × V)
Theorem	grlimdmrel 49217	The domain of the graph local isomorphism function is a relation. (Contributed by AV, 20-May-2025.)
⊢ Rel dom GraphLocIso
Definition	df-grlic 49218	Two graphs are said to be locally isomorphic iff they are connected by at least one local isomorphism. (Contributed by AV, 27-Apr-2025.)
⊢ ≃𝑙𝑔𝑟 = (◡ GraphLocIso “ (V ∖ 1o))
Theorem	isgrlim 49219*	A local isomorphism of graphs is a bijection between their vertices that preserves neighborhoods. (Contributed by AV, 20-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣))))))
Theorem	isgrlim2 49220*	A local isomorphism of graphs is a bijection between their vertices that preserves neighborhoods. Definitions expanded. (Contributed by AV, 29-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣))    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))))
Theorem	grlimprop 49221*	Properties of a local isomorphism of graphs. (Contributed by AV, 21-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))))
Theorem	grlimf1o 49222	A local isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 21-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
Theorem	grlimprop2 49223*	Properties of a local isomorphism of graphs. (Contributed by AV, 29-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣))    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))
Theorem	uhgrimgrlim 49224	An isomorphism of hypergraphs is a local isomorphism between the two graphs. (Contributed by AV, 2-Jun-2025.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
Theorem	uspgrlimlem1 49225*	Lemma 1 for uspgrlim 49229. (Contributed by AV, 16-Aug-2025.)
⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (𝐻 ∈ USPGraph → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
Theorem	uspgrlimlem2 49226*	Lemma 2 for uspgrlim 49229. (Contributed by AV, 16-Aug-2025.)
⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (𝐻 ∈ USPGraph → (◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
Theorem	uspgrlimlem3 49227*	Lemma 3 for uspgrlim 49229. (Contributed by AV, 16-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣))    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → (𝑒 ∈ 𝐾 → (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ◡(iEdg‘𝐺))‘𝑒)))
Theorem	uspgrlimlem4 49228*	Lemma 4 for uspgrlim 49229. (Contributed by AV, 16-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣))    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖))))
Theorem	uspgrlim 49229*	A local isomorphism of simple pseudographs is a bijection between their vertices that preserves neighborhoods, expressed by properties of their edges (not edge functions as in isgrlim2 49220). (Contributed by AV, 15-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣))    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))))
Theorem	usgrlimprop 49230*	Properties of a local isomorphism of simple pseudographs. (Contributed by AV, 17-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣))    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
Theorem	clnbgrvtxedg 49231*	An edge 𝐸 containing a vertex 𝐴 is an edge in the closed neighborhood of this vertex 𝐴. (Contributed by AV, 25-Dec-2025.)
⊢ 𝑁 = (𝐺 ClNeighbVtx 𝐴)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸) → 𝐸 ∈ 𝐾)
Theorem	grlimedgclnbgr 49232*	For two locally isomorphic graphs 𝐺 and 𝐻 and a vertex 𝐴 of 𝐺 there are two bijections 𝑓 and 𝑔 mapping the closed neighborhood 𝑁 of 𝐴 onto the closed neighborhood 𝑀 of (𝐹‘𝐴) and the edges between the vertices in 𝑁 onto the edges between the vertices in 𝑀, so that the mapped vertices of an edge 𝐸 containing the vertex 𝐴 is an edge between the vertices in 𝑀. (Contributed by AV, 25-Dec-2025.)
⊢ 𝑁 = (𝐺 ClNeighbVtx 𝐴)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝐴))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ (𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸)) → ∃𝑓∃𝑔(𝑓:𝑁–1-1-onto→𝑀 ∧ 𝑔:𝐾–1-1-onto→𝐿 ∧ (𝑓 “ 𝐸) = (𝑔‘𝐸)))
Theorem	grlimprclnbgr 49233*	For two locally isomorphic graphs 𝐺 and 𝐻 and a vertex 𝐴 of 𝐺 there are two bijections 𝑓 and 𝑔 mapping the closed neighborhood 𝑁 of 𝐴 onto the closed neighborhood 𝑀 of (𝐹‘𝐴) and the edges between the vertices in 𝑁 onto the edges between the vertices in 𝑀, so that the mapped vertices of an edge {𝐴, 𝐵} containing the vertex 𝐴 is an edge between the vertices in 𝑀. (Contributed by AV, 25-Dec-2025.)
⊢ 𝑁 = (𝐺 ClNeighbVtx 𝐴)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝐴))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ {𝐴, 𝐵} ∈ 𝐼)) → ∃𝑓∃𝑔(𝑓:𝑁–1-1-onto→𝑀 ∧ 𝑔:𝐾–1-1-onto→𝐿 ∧ {(𝑓‘𝐴), (𝑓‘𝐵)} = (𝑔‘{𝐴, 𝐵})))
Theorem	grlimprclnbgredg 49234*	For two locally isomorphic graphs 𝐺 and 𝐻 and a vertex 𝐴 of 𝐺 there is a bijection 𝑓 mapping the closed neighborhood 𝑁 of 𝐴 onto the closed neighborhood 𝑀 of (𝐹‘𝐴), so that the mapped vertices of an edge {𝐴, 𝐵} containing the vertex 𝐴 is an edge between the vertices in 𝑀. (Contributed by AV, 27-Dec-2025.)
⊢ 𝑁 = (𝐺 ClNeighbVtx 𝐴)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝐴))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ {𝐴, 𝐵} ∈ 𝐼)) → ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ {(𝑓‘𝐴), (𝑓‘𝐵)} ∈ 𝐿))
Theorem	grlimpredg 49235*	For two locally isomorphic graphs 𝐺 and 𝐻 and a vertex 𝐴 of 𝐺 there is a bijection 𝑓 mapping the closed neighborhood 𝑁 of 𝐴 onto the closed neighborhood 𝑀 of (𝐹‘𝐴), so that the mapped vertices of an edge {𝐴, 𝐵} containing the vertex 𝐴 is an edge in 𝐻. (Contributed by AV, 27-Dec-2025.)
⊢ 𝑁 = (𝐺 ClNeighbVtx 𝐴)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝐴))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ {𝐴, 𝐵} ∈ 𝐼)) → ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ {(𝑓‘𝐴), (𝑓‘𝐵)} ∈ 𝐽))
Theorem	grlimprclnbgrvtx 49236*	For two locally isomorphic graphs 𝐺 and 𝐻 and a vertex 𝐴 of 𝐺 there is a bijection 𝑓 mapping the closed neighborhood 𝑁 of 𝐴 onto the closed neighborhood 𝑀 of (𝐹‘𝐴), so that the mapped vertices of an edge {𝐴, 𝐵} containing the vertex 𝐴 is an edge between the vertices in 𝑀 containing the vertex (𝐹‘𝐴). (Contributed by AV, 28-Dec-2025.)
⊢ 𝑁 = (𝐺 ClNeighbVtx 𝐴)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝐴))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ {𝐴, 𝐵} ∈ 𝐼)) → ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ({(𝐹‘𝐴), (𝑓‘𝐵)} ∈ 𝐿 ∨ {(𝐹‘𝐴), (𝑓‘𝐴)} ∈ 𝐿)))
Theorem	grlimgredgex 49237*	Local isomorphisms between simple pseudographs map an edge onto an edge with an endpoint being the image of one of the endpoints of the first edge under the local isomorphism. (Contributed by AV, 28-Dec-2025.)
⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝐼)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ 𝑉 {(𝐹‘𝐴), 𝑣} ∈ 𝐸)
Theorem	grlimgrtrilem1 49238*	Lemma 3 for grlimgrtri 49240. (Contributed by AV, 24-Aug-2025.) (Proof shortened by AV, 27-Dec-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ 𝐼 ∧ {𝑎, 𝑐} ∈ 𝐼 ∧ {𝑏, 𝑐} ∈ 𝐼)) → ({𝑎, 𝑏} ∈ 𝐾 ∧ {𝑎, 𝑐} ∈ 𝐾 ∧ {𝑏, 𝑐} ∈ 𝐾))
Theorem	grlimgrtrilem2 49239*	Lemma 3 for grlimgrtri 49240. (Contributed by AV, 23-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑎))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝑓:𝑁–1-1-onto→𝑀 ∧ 𝑔:𝐾–1-1-onto→𝐿) ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ 𝐾) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ 𝐽)
Theorem	grlimgrtri 49240*	If one of two locally isomorphic graphs has a triangle, so does the other. The triangle in the other graph is not necessarily the image (𝐹 “ 𝑇) of the triangle 𝑇 in the first graph. (Contributed by AV, 24-Aug-2025.)
⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺))    ⇒   ⊢ (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻))
Theorem	brgrlic 49241	The relation "is locally isomorphic to" for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ (𝑅 GraphLocIso 𝑆) ≠ ∅)
Theorem	brgrilci 49242	Prove that two graphs are locally isomorphic by an explicit local isomorphism. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐹 ∈ (𝑅 GraphLocIso 𝑆) → 𝑅 ≃𝑙𝑔𝑟 𝑆)
Theorem	grlicrel 49243	The "is locally isomorphic to" relation for graphs is a relation. (Contributed by AV, 9-Jun-2025.)
⊢ Rel ≃𝑙𝑔𝑟
Theorem	grlicrcl 49244	Reverse closure of the "is locally isomorphic to" relation for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ≃𝑙𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgrlic2 49245*	Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))))
Theorem	grilcbri 49246*	Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))))
Theorem	dfgrlic3 49247*	Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝑓‘𝑣))    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑗(𝑗:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑗 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))))
Theorem	grilcbri2 49248*	Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝑓‘𝑋))    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ (𝑋 ∈ 𝑉 → ∃𝑗(𝑗:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑗 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))))
Theorem	grlicref 49249	Graph local isomorphism is reflexive for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑙𝑔𝑟 𝐺)
Theorem	grlicsym 49250	Graph local isomorphism is symmetric for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑙𝑔𝑟 𝑆 → 𝑆 ≃𝑙𝑔𝑟 𝐺))
Theorem	grlicsymb 49251	Graph local isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph) → (𝐴 ≃𝑙𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑙𝑔𝑟 𝐴))
Theorem	grlictr 49252	Graph local isomorphism is transitive. (Contributed by AV, 10-Jun-2025.)
⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → 𝑅 ≃𝑙𝑔𝑟 𝑇)
Theorem	grlicer 49253	Local isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 11-Jun-2025.)
⊢ ( ≃𝑙𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph
Theorem	grlicen 49254	Locally isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 11-Jun-2025.)
⊢ 𝐵 = (Vtx‘𝑅)    &   ⊢ 𝐶 = (Vtx‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶)
Theorem	gricgrlic 49255	Isomorphic hypergraphs are locally isomorphic. (Contributed by AV, 12-Jun-2025.) (Proof shortened by AV, 11-Jul-2025.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐺 ≃𝑔𝑟 𝐻 → 𝐺 ≃𝑙𝑔𝑟 𝐻))
Theorem	clnbgr3stgrgrlim 49256*	If all (closed) neighborhoods of the vertices in two simple graphs with the same order induce a subgraph which is isomorphic to an 𝑁-star, then any bijection between the vertices is a local isomorphism between the two graphs. (Contributed by AV, 28-Dec-2025.)
⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟 (StarGr‘𝑁) ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟 (StarGr‘𝑁)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
Theorem	clnbgr3stgrgrlic 49257*	If all (closed) neighborhoods of the vertices in two simple graphs with the same order induce a subgraph which is isomorphic to an 𝑁-star, then the two graphs are locally isomorphic. (Contributed by AV, 29-Sep-2025.)
⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟 (StarGr‘𝑁) ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟 (StarGr‘𝑁)) → 𝐺 ≃𝑙𝑔𝑟 𝐻)
Theorem	usgrexmpl1lem 49258*	Lemma for usgrexmpl1 49259. (Contributed by AV, 2-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    ⇒   ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
Theorem	usgrexmpl1 49259	𝐺 is a simple graph of six vertices 0, 1, 2, 3, 4, 5, with edges {0, 1}, {1, 2}, {0, 2}, {0, 3}, {3, 4}, {3, 5}, {4, 5}. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐺 ∈ USGraph
Theorem	usgrexmpl1vtx 49260	The vertices 0, 1, 2, 3, 4, 5 of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Vtx‘𝐺) = ({0, 1, 2} ∪ {3, 4, 5})
Theorem	usgrexmpl1edg 49261	The edges {0, 1}, {1, 2}, {0, 2}, {0, 3}, {3, 4}, {3, 5}, {4, 5} of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Edg‘𝐺) = ({{0, 3}} ∪ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4, 5}}))
Theorem	usgrexmpl1tri 49262	𝐺 contains a triangle 0, 1, 2, with corresponding edges {0, 1}, {1, 2}, {0, 2}. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ {0, 1, 2} ∈ (GrTriangles‘𝐺)
Theorem	usgrexmpl2lem 49263*	Lemma for usgrexmpl2 49264. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    ⇒   ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
Theorem	usgrexmpl2 49264	𝐺 is a simple graph of six vertices 0, 1, 2, 3, 4, 5, with edges {0, 1}, {1, 2}, {2, 3}, {0, 3}, {3, 4}, {4, 5}, {0, 5}. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐺 ∈ USGraph
Theorem	usgrexmpl2vtx 49265	The vertices 0, 1, 2, 3, 4, 5 of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Vtx‘𝐺) = ({0, 1, 2} ∪ {3, 4, 5})
Theorem	usgrexmpl2edg 49266	The edges {0, 1}, {1, 2}, {2, 3}, {0, 3}, {3, 4}, {4, 5}, {0, 5} of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 3-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Edg‘𝐺) = ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))
Theorem	usgrexmpl2nblem 49267*	Lemma for usgrexmpl2nb0 49268 etc. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐾 ∈ ({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 𝐾) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣ {𝐾, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))})
Theorem	usgrexmpl2nb0 49268	The neighborhood of the first vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 0) = {1, 3, 5}
Theorem	usgrexmpl2nb1 49269	The neighborhood of the second vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 1) = {0, 2}
Theorem	usgrexmpl2nb2 49270	The neighborhood of the third vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 2) = {1, 3}
Theorem	usgrexmpl2nb3 49271	The neighborhood of the forth vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 3) = {0, 2, 4}
Theorem	usgrexmpl2nb4 49272	The neighborhood of the fifth vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 4) = {3, 5}
Theorem	usgrexmpl2nb5 49273	The neighborhood of the sixth vertex of graph 𝐺. (Contributed by AV, 10-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (𝐺 NeighbVtx 5) = {0, 4}
Theorem	usgrexmpl2trifr 49274*	𝐺 is triangle-free. (Contributed by AV, 10-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ¬ ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺)
Theorem	usgrexmpl12ngric 49275	The graphs 𝐻 and 𝐺 are not isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 49262, whereas 𝐺 does not, see usgrexmpl2trifr 49274. (Contributed by AV, 10-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    &   ⊢ 𝐾 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐻 = ⟨𝑉, 𝐾⟩    ⇒   ⊢ ¬ 𝐺 ≃𝑔𝑟 𝐻
Theorem	usgrexmpl12ngrlic 49276	The graphs 𝐻 and 𝐺 are not locally isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 49262, whereas 𝐺 does not, see usgrexmpl2trifr 49274. (Contributed by AV, 24-Aug-2025.)
⊢ 𝑉 = (0...5)    &   ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    &   ⊢ 𝐾 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩    &   ⊢ 𝐻 = ⟨𝑉, 𝐾⟩    ⇒   ⊢ ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻
21.52.15.8  Generalized Petersen graphs According to Wikipedia "Generalized Petersen graph", 26-Aug-2025, https://en.wikipedia.org/wiki/Generalized_Petersen_graph: "In graph theory, the generalized Petersen graphs are a family of cubic graphs formed by connecting the vertices of a regular polygon to the corresponding vertices of a star polygon. They include the Petersen graph and generalize one of the ways of constructing the Petersen graph. ... Among the generalized Petersen graphs are the n-prism, ...". The vertices of the regular polygon are called "outside vertices", the vertices of the star polygon "inside vertices" (see A. Steimle, W. Stanton, "The isomorphism classes of the generalized Petersen graphs", Discrete Mathematics Volume 309, Issue 1, 6 January 2009, Pages 231-237: https://doi.org/10.1016/j.disc.2007.12.074). Since regular polygons are also considered as star polygons (with density 1), many theorems for "inside vertices" (with labels containing the fragment "vtx1") can be specialized for "outside vertices" (with labels containing the fragment "vtx0").
Syntax	cgpg 49277	Extend class notation with generalized Petersen graphs.
class gPetersenGr
Definition	df-gpg 49278*	Definition of generalized Petersen graphs according to Wikipedia "Generalized Petersen graph", 26-Aug-2025, https://en.wikipedia.org/wiki/Generalized_Petersen_graph: "In Watkins' notation, 𝐺(𝑛, 𝑘) is a graph with vertex set { u0, u1, ... , un-1, v0, v1, ... , vn-1 } and edge set { ui ui+1 , ui vi , vi vi+k | 0 ≤ 𝑖 ≤ (𝑛 − 1) } where subscripts are to be read modulo n and where 𝑘 < (𝑛 / 2). Some authors use the notation GPG(n,k)." Instead of 𝑛 ∈ ℕ, we could restrict the first argument to 𝑛 ∈ (ℤ≥‘3) (i.e., 3 ≤ 𝑛), because for 𝑛 ≤ 2, the definition is not meaningful (since then (⌈‘(𝑛 / 2)) ≤ 1 and therefore (1..^(⌈‘(𝑛 / 2))) = ∅, so that there would be no fitting second argument). (Contributed by AV, 26-Aug-2025.)
⊢ gPetersenGr = (𝑛 ∈ ℕ, 𝑘 ∈ (1..^(⌈‘(𝑛 / 2))) ↦ {⟨(Base‘ndx), ({0, 1} × (0..^𝑛))⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑛)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝑘) mod 𝑛)⟩})})⟩})
Theorem	gpgov 49279*	The generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (𝑁 gPetersenGr 𝐾) = {⟨(Base‘ndx), ({0, 1} × 𝐼)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})⟩})
Theorem	gpgvtx 49280	The vertices of the generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (Vtx‘(𝑁 gPetersenGr 𝐾)) = ({0, 1} × 𝐼))
Theorem	gpgiedg 49281*	The indexed edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (iEdg‘(𝑁 gPetersenGr 𝐾)) = ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})}))
Theorem	gpgedg 49282*	The edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (Edg‘(𝑁 gPetersenGr 𝐾)) = {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})})
Theorem	gpgiedgdmellem 49283*	Lemma for gpgiedgdmel 49286 and gpgedgel 49287. (Contributed by AV, 2-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (∃𝑥 ∈ 𝐼 (𝑌 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑌 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑌 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩}) → 𝑌 ∈ 𝒫 ({0, 1} × 𝐼)))
Theorem	gpgvtxel 49284*	A vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 29-Aug-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → (𝑋 ∈ 𝑉 ↔ ∃𝑥 ∈ {0, 1}∃𝑦 ∈ 𝐼 𝑋 = ⟨𝑥, 𝑦⟩))
Theorem	gpgvtxel2 49285	The second component of a vertex in a generalized Petersen graph 𝐺. (Contributed by AV, 30-Aug-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑉) → (2nd ‘𝑋) ∈ 𝐼)
Theorem	gpgiedgdmel 49286*	An index of edges of the generalized Petersen graph GPG(N,K). (Contributed by AV, 2-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (𝑋 ∈ dom (iEdg‘𝐺) ↔ ∃𝑥 ∈ 𝐼 (𝑋 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑋 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑋 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})))
Theorem	gpgedgel 49287*	An edge in a generalized Petersen graph 𝐺. (Contributed by AV, 29-Aug-2025.) (Proof shortened by AV, 8-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → (𝑌 ∈ 𝐸 ↔ ∃𝑥 ∈ 𝐼 (𝑌 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑌 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑌 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})))
Theorem	gpgprismgriedgdmel 49288*	An index of edges of the generalized Petersen graph GPG(N,1). (Contributed by AV, 2-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐺 = (𝑁 gPetersenGr 1)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑋 ∈ dom (iEdg‘𝐺) ↔ ∃𝑥 ∈ 𝐼 (𝑋 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑋 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑋 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 1) mod 𝑁)⟩})))
Theorem	gpgprismgriedgdmss 49289	A subset of the index of edges of the generalized Petersen graph GPG(N,1). (Contributed by AV, 2-Nov-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → ({{⟨0, 0⟩, ⟨0, 1⟩}, {⟨0, 0⟩, ⟨1, 0⟩}} ∪ {{⟨1, 1⟩, ⟨0, 1⟩}, {⟨1, 1⟩, ⟨1, 0⟩}}) ⊆ dom (iEdg‘(𝑁 gPetersenGr 1)))
Theorem	gpgvtx0 49290	The outside vertices in a generalized Petersen graph 𝐺. (Contributed by AV, 30-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑉) → (⟨0, (((2nd ‘𝑋) + 1) mod 𝑁)⟩ ∈ 𝑉 ∧ ⟨0, (2nd ‘𝑋)⟩ ∈ 𝑉 ∧ ⟨0, (((2nd ‘𝑋) − 1) mod 𝑁)⟩ ∈ 𝑉))
Theorem	gpgvtx1 49291	The inside vertices in a generalized Petersen graph 𝐺. (Contributed by AV, 28-Aug-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) ∧ 𝑋 ∈ 𝑉) → (⟨1, (((2nd ‘𝑋) + 𝐾) mod 𝑁)⟩ ∈ 𝑉 ∧ ⟨1, (2nd ‘𝑋)⟩ ∈ 𝑉 ∧ ⟨1, (((2nd ‘𝑋) − 𝐾) mod 𝑁)⟩ ∈ 𝑉))
Theorem	opgpgvtx 49292	A vertex in a generalized Petersen graph 𝐺 as ordered pair. (Contributed by AV, 1-Oct-2025.)
⊢ 𝐼 = (0..^𝑁)    &   ⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → (⟨𝑋, 𝑌⟩ ∈ 𝑉 ↔ ((𝑋 = 0 ∨ 𝑋 = 1) ∧ 𝑌 ∈ 𝐼)))
Theorem	gpgusgralem 49293*	Lemma for gpgusgra 49294. (Contributed by AV, 27-Aug-2025.) (Proof shortened by AV, 6-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ 𝐽) → {𝑒 ∈ 𝒫 ({0, 1} × 𝐼) ∣ ∃𝑥 ∈ 𝐼 (𝑒 = {⟨0, 𝑥⟩, ⟨0, ((𝑥 + 1) mod 𝑁)⟩} ∨ 𝑒 = {⟨0, 𝑥⟩, ⟨1, 𝑥⟩} ∨ 𝑒 = {⟨1, 𝑥⟩, ⟨1, ((𝑥 + 𝐾) mod 𝑁)⟩})} ⊆ {𝑝 ∈ 𝒫 ({0, 1} × 𝐼) ∣ (♯‘𝑝) = 2})
Theorem	gpgusgra 49294	The generalized Petersen graph GPG(N,K) is a simple graph. (Contributed by AV, 27-Aug-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (𝑁 gPetersenGr 𝐾) ∈ USGraph)
Theorem	gpgprismgrusgra 49295	The generalized Petersen graphs G(N,1), which are the N-prisms, are simple graphs. (Contributed by AV, 31-Oct-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 gPetersenGr 1) ∈ USGraph)
Theorem	gpgorder 49296	The order of the generalized Petersen graph GPG(N,K). (Contributed by AV, 29-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽) → (♯‘(Vtx‘(𝑁 gPetersenGr 𝐾))) = (2 · 𝑁))
Theorem	gpg5order 49297	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 49298	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 49299	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 49300	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 𝑁)⟩))