P. 485 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48401-48500   *Has distinct variable group(s)

Type	Label	Description
Statement
21.48.15.5  Triangles in graphs Usually, a "triangle" in graph theory is a complete graph consisting of three vertices (denoted by " K3 "), see the definition in [Diestel] p. 3 or the definition in [Bollobas] p. 5. This corresponds to the definition of a "triangle graph" (which is a more precise term) in Wikipedia "Triangle graph", https://en.wikipedia.org/wiki/Triangle_graph, 27-Jul-2025: "In the mathematical field of graph theory, the triangle graph is a planar undirected graph with 3 vertices and 3 edges, in the form of a triangle. The triangle graph is also known as the cycle graph C3 and the complete graph K3." Often, however, the term "triangle" is also used to denote a corresponding subgraph of a given graph ("triangle in a graph"), see, for example, Wikipedia "Triangle-free graph", 28-Jul-2025, https://en.wikipedia.org/wiki/Triangle-free_graph: "In the mathematical area of graph theory, a triangle-free graph is an undirected graph in which no three vertices form a triangle of edges." In this subsection, a triangle (in a graph) is defined as a set of three vertices of a given graph. In this meaning, a triangle 𝑇 with (𝑇 ∈ (GrTriangles‘𝐺)) is neither a graph nor a subgraph, but it induces a triangle graph (𝐺 ISubGr 𝑇) as subgraph of the given graph 𝐺. We require that there are three (different) edges connecting the three (different) vertices of the triangle. Therefore, it is not sufficient for arbitrary hypergraphs to say "a triangle is a set of three (different) vertices connected with each other (by edges)", because there might be only one or two multiedges fulfilling this statement. We do not regard such degenerate cases as "triangle". The definition df-grtri 48402 is designed for a special purpose, namely to provide a criterion for two graphs being not isomorphic (see grimgrtri 48413). For other purposes, a more general definition might be useful, e.g., ComplSubGr = (𝑔 ∈ V, 𝑛 ∈ ℕ ↦ {𝑡 ∈ 𝒫 𝑣 ∣ ((♯‘𝑡) = 𝑛 ∧ (𝑔 ISubGr 𝑡) ∈ ComplGraph)}) for complete subgraphs of a given size (proposed by TA). With such a definition, we would have (GrTriangles‘𝐺) = (𝐺 ComplSubGr 3) (at least for simple graphs), and the definition df-grtri 48402 may become obsolete.
Syntax	cgrtri 48401	Extend class notation with triangles (in a graph).
class GrTriangles
Definition	df-grtri 48402*	Definition of a triangles in a graph. A triangle in a graph is a set of three (different) vertices completely connected with each other. Such vertices induce a closed walk of length 3, see grtriclwlk3 48409, and the vertices of a cycle of size 3 are a triangle in a graph, see cycl3grtri 48411. (Contributed by AV, 20-Jul-2025.)
⊢ GrTriangles = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))})
Theorem	grtriproplem 48403	Lemma for grtriprop 48405. (Contributed by AV, 23-Jul-2025.)
⊢ ((𝑓:(0..^3)–1-1-onto→{𝑥, 𝑦, 𝑧} ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝐸 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝐸 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝐸)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))
Theorem	grtri 48404*	The triangles in a graph. (Contributed by AV, 20-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (GrTriangles‘𝐺) = {𝑡 ∈ 𝒫 𝑉 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝐸 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝐸 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝐸))})
Theorem	grtriprop 48405*	The properties of a triangle. (Contributed by AV, 25-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
Theorem	grtrif1o 48406	Any bijection onto a triangle preserves the edges of the triangle. (Contributed by AV, 25-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (GrTriangles‘𝐺) ∧ 𝐹:(0..^3)–1-1-onto→𝑇) → ({(𝐹‘0), (𝐹‘1)} ∈ 𝐸 ∧ {(𝐹‘0), (𝐹‘2)} ∈ 𝐸 ∧ {(𝐹‘1), (𝐹‘2)} ∈ 𝐸))
Theorem	isgrtri 48407*	A triangle in a graph. (Contributed by AV, 20-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
Theorem	grtrissvtx 48408	A triangle is a subset of the vertices (of a graph). (Contributed by AV, 26-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → 𝑇 ⊆ 𝑉)
Theorem	grtriclwlk3 48409	A triangle induces a closed walk of length 3 . (Contributed by AV, 26-Jul-2025.)
⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺))    &   ⊢ (𝜑 → 𝑃:(0..^3)–1-1-onto→𝑇)    ⇒   ⊢ (𝜑 → 𝑃 ∈ (3 ClWWalksN 𝐺))
Theorem	cycl3grtrilem 48410	Lemma for cycl3grtri 48411. (Contributed by AV, 5-Oct-2025.)
⊢ (((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ∧ (♯‘𝐹) = 3)) → ({(𝑃‘0), (𝑃‘1)} ∈ (Edg‘𝐺) ∧ {(𝑃‘0), (𝑃‘2)} ∈ (Edg‘𝐺) ∧ {(𝑃‘1), (𝑃‘2)} ∈ (Edg‘𝐺)))
Theorem	cycl3grtri 48411	The vertices of a cycle of size 3 are a triangle in a graph. (Contributed by AV, 5-Oct-2025.)
⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)    &   ⊢ (𝜑 → (♯‘𝐹) = 3)    ⇒   ⊢ (𝜑 → ran 𝑃 ∈ (GrTriangles‘𝐺))
Theorem	grtrimap 48412	Conditions for mapping triangles onto triangles. Lemma for grimgrtri 48413 and grlimgrtri 48467. (Contributed by AV, 23-Aug-2025.)
⊢ (𝐹:𝑉–1-1→𝑊 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)) → (((𝐹‘𝑎) ∈ 𝑊 ∧ (𝐹‘𝑏) ∈ 𝑊 ∧ (𝐹‘𝑐) ∈ 𝑊) ∧ (𝐹 “ 𝑇) = {(𝐹‘𝑎), (𝐹‘𝑏), (𝐹‘𝑐)} ∧ (♯‘(𝐹 “ 𝑇)) = 3)))
Theorem	grimgrtri 48413	Graph isomorphisms map triangles onto triangles. (Contributed by AV, 27-Jul-2025.) (Proof shortened by AV, 24-Aug-2025.)
⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺))    ⇒   ⊢ (𝜑 → (𝐹 “ 𝑇) ∈ (GrTriangles‘𝐻))
Theorem	usgrgrtrirex 48414*	Conditions for a simple graph to contain a triangle. (Contributed by AV, 7-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑎)    ⇒   ⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
21.48.15.6  Star graphs According to Wikipedia "Star (graph theory)", 10-Sep-2025, https://en.wikipedia.org/wiki/Star_(graph_theory): "In graph theory, the star Sk is the complete bipartite graph K(1,k), that is, it is a tree with one internal node and k leaves. Alternatively, some authors define Sk to be the tree of order k with maximum diameter 2, in which case a star of k > 2 has k - 1 leaves.".
Syntax	cstgr 48415	Extend class notation with star graphs.
class StarGr
Definition	df-stgr 48416*	Definition of star graphs according to the first definition in Wikipedia, so that (StarGr‘𝑁) has size 𝑁, and order 𝑁 + 1: (StarGr‘0) will be a single vertex (graph without edges), see stgr0 48424, (StarGr‘1) will be a single edge (graph with two vertices connected by an edge), see stgr1 48425, and (StarGr‘3) will be a 3-star or "claw" (a star with 3 edges). (Contributed by AV, 10-Sep-2025.)
⊢ StarGr = (𝑛 ∈ ℕ0 ↦ {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩})
Theorem	stgrfv 48417*	The star graph SN. (Contributed by AV, 10-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) = {⟨(Base‘ndx), (0...𝑁)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})⟩})
Theorem	stgrvtx 48418	The vertices of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Vtx‘(StarGr‘𝑁)) = (0...𝑁))
Theorem	stgriedg 48419*	The indexed edges of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (iEdg‘(StarGr‘𝑁)) = ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}))
Theorem	stgredg 48420*	The edges of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})
Theorem	stgredgel 48421*	An edge of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (𝐸 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐸 ⊆ (0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝐸 = {0, 𝑥})))
Theorem	stgredgiun 48422*	The edges of the star graph SN as indexed union. (Contributed by AV, 29-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = ∪ 𝑥 ∈ (1...𝑁){{0, 𝑥}})
Theorem	stgrusgra 48423	The star graph SN is a simple graph. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) ∈ USGraph)
Theorem	stgr0 48424	The star graph S0 consists of a single vertex without edges. (Contributed by AV, 11-Sep-2025.)
⊢ (StarGr‘0) = {⟨(Base‘ndx), {0}⟩, ⟨(.ef‘ndx), ∅⟩}
Theorem	stgr1 48425	The star graph S1 consists of a single simple edge. (Contributed by AV, 11-Sep-2025.)
⊢ (StarGr‘1) = {⟨(Base‘ndx), {0, 1}⟩, ⟨(.ef‘ndx), ( I ↾ {{0, 1}})⟩}
Theorem	stgrvtx0 48426	The center ("internal node") of a star graph SN. (Contributed by AV, 12-Sep-2025.)
⊢ 𝐺 = (StarGr‘𝑁)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 0 ∈ 𝑉)
Theorem	stgrorder 48427	The order of a star graph SN. (Contributed by AV, 12-Sep-2025.)
⊢ 𝐺 = (StarGr‘𝑁)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (♯‘𝑉) = (𝑁 + 1))
Theorem	stgrnbgr0 48428	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 48429	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 48430	Lemma 1 for isubgr3stgr 48439. (Contributed by AV, 16-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝐹 = (𝐻 ∪ {⟨𝑋, 𝑌⟩})    ⇒   ⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐹:𝐶–1-1-onto→(𝑅 ∪ {𝑌}))
Theorem	isubgr3stgrlem2 48431*	Lemma 2 for isubgr3stgr 48439. (Contributed by AV, 16-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}))
Theorem	isubgr3stgrlem3 48432*	Lemma 3 for isubgr3stgr 48439. (Contributed by AV, 17-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0))
Theorem	isubgr3stgrlem4 48433*	Lemma 4 for isubgr3stgr 48439. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐴 = 𝑋 ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧})
Theorem	isubgr3stgrlem5 48434*	Lemma 5 for isubgr3stgr 48439. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((𝐹:𝐶⟶𝑊 ∧ 𝑌 ∈ 𝐼) → (𝐻‘𝑌) = (𝐹 “ 𝑌))
Theorem	isubgr3stgrlem6 48435*	Lemma 6 for isubgr3stgr 48439. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼⟶(Edg‘(StarGr‘𝑁)))
Theorem	isubgr3stgrlem7 48436*	Lemma 7 for isubgr3stgr 48439. (Contributed by AV, 29-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝐽) ∈ 𝐼)
Theorem	isubgr3stgrlem8 48437*	Lemma 8 for isubgr3stgr 48439. (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 48438*	Lemma 9 for isubgr3stgr 48439. (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 48439*	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.48.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 48451. This definition is according to a chat in mathoverflow (https://mathoverflow.net/questions/491133/locally-isomorphic-graphs 48451): roughly speaking, it restricts the correspondence of two graphs to their neighborhoods. Additionally, a binary relation ≃𝑙𝑔𝑟 is defined (see df-grlic 48445) 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 48480. The names and symbols are chosen analogously to group isomorphisms GrpIso (see df-gim 19223) and graph isomorphisms GraphIso (see df-grim 48342) resp. isomorphism between groups ≃𝑔 (see df-gic 19224) and isomorphism between graphs ≃𝑔𝑟 (see df-gric 48345). 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 48593. Such two graphs are the two generalized Petersen graphs G(5,K) of order 10 (see definition df-gpg 48505), which are the Petersen graph G(5,2) and the 5-prism G(5,1), see gpg5ngric 48592.
Syntax	cgrlim 48440	The class of graph local isomorphism sets.
class GraphLocIso
Syntax	cgrlic 48441	The class of the graph local isomorphism relation.
class ≃𝑙𝑔𝑟
Definition	df-grlim 48442*	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 48443	The graph local isomorphism function is a well-defined function. (Contributed by AV, 20-May-2025.)
⊢ GraphLocIso Fn (V × V)
Theorem	grlimdmrel 48444	The domain of the graph local isomorphism function is a relation. (Contributed by AV, 20-May-2025.)
⊢ Rel dom GraphLocIso
Definition	df-grlic 48445	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 48446*	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 48447*	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 48448*	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 48449	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 48450*	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 48451	An isomorphism of hypergraphs is a local isomorphism between the two graphs. (Contributed by AV, 2-Jun-2025.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
Theorem	uspgrlimlem1 48452*	Lemma 1 for uspgrlim 48456. (Contributed by AV, 16-Aug-2025.)
⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (𝐻 ∈ USPGraph → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
Theorem	uspgrlimlem2 48453*	Lemma 2 for uspgrlim 48456. (Contributed by AV, 16-Aug-2025.)
⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (𝐻 ∈ USPGraph → (◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
Theorem	uspgrlimlem3 48454*	Lemma 3 for uspgrlim 48456. (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 48455*	Lemma 4 for uspgrlim 48456. (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 48456*	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 48447). (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 48457*	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 48458*	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 48459*	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 48460*	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 48461*	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 48462*	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 48463*	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 48464*	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 48465*	Lemma 3 for grlimgrtri 48467. (Contributed by AV, 24-Aug-2025.) (Proof shortened by AV, 27-Dec-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ 𝐼 ∧ {𝑎, 𝑐} ∈ 𝐼 ∧ {𝑏, 𝑐} ∈ 𝐼)) → ({𝑎, 𝑏} ∈ 𝐾 ∧ {𝑎, 𝑐} ∈ 𝐾 ∧ {𝑏, 𝑐} ∈ 𝐾))
Theorem	grlimgrtrilem2 48466*	Lemma 3 for grlimgrtri 48467. (Contributed by AV, 23-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑎))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝑓:𝑁–1-1-onto→𝑀 ∧ 𝑔:𝐾–1-1-onto→𝐿) ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ 𝐾) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ 𝐽)
Theorem	grlimgrtri 48467*	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 48468	The relation "is locally isomorphic to" for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ (𝑅 GraphLocIso 𝑆) ≠ ∅)
Theorem	brgrilci 48469	Prove that two graphs are locally isomorphic by an explicit local isomorphism. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐹 ∈ (𝑅 GraphLocIso 𝑆) → 𝑅 ≃𝑙𝑔𝑟 𝑆)
Theorem	grlicrel 48470	The "is locally isomorphic to" relation for graphs is a relation. (Contributed by AV, 9-Jun-2025.)
⊢ Rel ≃𝑙𝑔𝑟
Theorem	grlicrcl 48471	Reverse closure of the "is locally isomorphic to" relation for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ≃𝑙𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgrlic2 48472*	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 48473*	Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))))
Theorem	dfgrlic3 48474*	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 48475*	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 48476	Graph local isomorphism is reflexive for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑙𝑔𝑟 𝐺)
Theorem	grlicsym 48477	Graph local isomorphism is symmetric for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑙𝑔𝑟 𝑆 → 𝑆 ≃𝑙𝑔𝑟 𝐺))
Theorem	grlicsymb 48478	Graph local isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 9-Jun-2025.)
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph) → (𝐴 ≃𝑙𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑙𝑔𝑟 𝐴))
Theorem	grlictr 48479	Graph local isomorphism is transitive. (Contributed by AV, 10-Jun-2025.)
⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → 𝑅 ≃𝑙𝑔𝑟 𝑇)
Theorem	grlicer 48480	Local isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 11-Jun-2025.)
⊢ ( ≃𝑙𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph
Theorem	grlicen 48481	Locally isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 11-Jun-2025.)
⊢ 𝐵 = (Vtx‘𝑅)    &   ⊢ 𝐶 = (Vtx‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶)
Theorem	gricgrlic 48482	Isomorphic hypergraphs are locally isomorphic. (Contributed by AV, 12-Jun-2025.) (Proof shortened by AV, 11-Jul-2025.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐺 ≃𝑔𝑟 𝐻 → 𝐺 ≃𝑙𝑔𝑟 𝐻))
Theorem	clnbgr3stgrgrlim 48483*	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 48484*	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 48485*	Lemma for usgrexmpl1 48486. (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 48486	𝐺 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 48487	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 48488	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 48489	𝐺 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 48490*	Lemma for usgrexmpl2 48491. (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 48491	𝐺 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 48492	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 48493	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 48494*	Lemma for usgrexmpl2nb0 48495 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 48495	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 48496	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 48497	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 48498	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 48499	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 48500	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}