P. 488 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48701-48800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	upgrimpthslem2 48701*	Lemma 2 for upgrimpths 48702. (Contributed by AV, 31-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (1..^(♯‘𝐹))) → (¬ ((𝑁 ∘ 𝑃)‘𝑋) = ((𝑁 ∘ 𝑃)‘0) ∧ ¬ ((𝑁 ∘ 𝑃)‘𝑋) = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))))
Theorem	upgrimpths 48702*	Graph isomorphisms between simple pseudographs map paths onto paths. (Contributed by AV, 31-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐸(Paths‘𝐻)(𝑁 ∘ 𝑃))
Theorem	upgrimspths 48703*	Graph isomorphisms between simple pseudographs map simple paths onto simple paths. (Contributed by AV, 31-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(SPaths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐸(SPaths‘𝐻)(𝑁 ∘ 𝑃))
Theorem	upgrimcycls 48704*	Graph isomorphisms between simple pseudographs map cycles onto cycles. (Contributed by AV, 31-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐸(Cycles‘𝐻)(𝑁 ∘ 𝑃))
Theorem	brgric 48705	The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.)
⊢ (𝑅 ≃𝑔𝑟 𝑆 ↔ (𝑅 GraphIso 𝑆) ≠ ∅)
Theorem	brgrici 48706	Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.)
⊢ (𝐹 ∈ (𝑅 GraphIso 𝑆) → 𝑅 ≃𝑔𝑟 𝑆)
Theorem	gricrcl 48707	Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025.)
⊢ (𝐺 ≃𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgric2 48708*	Alternate, explicit definition of the "is isomorphic to" relation for two graphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.)
⊢ 𝑉 = (Vtx‘𝐴)    &   ⊢ 𝑊 = (Vtx‘𝐵)    &   ⊢ 𝐼 = (iEdg‘𝐴)    &   ⊢ 𝐽 = (iEdg‘𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴 ≃𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))
Theorem	gricbri 48709*	Implications of two graphs being isomorphic. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.) (Proof shortened by AV, 12-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐴)    &   ⊢ 𝑊 = (Vtx‘𝐵)    &   ⊢ 𝐼 = (iEdg‘𝐴)    &   ⊢ 𝐽 = (iEdg‘𝐵)    ⇒   ⊢ (𝐴 ≃𝑔𝑟 𝐵 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))
Theorem	gricushgr 48710*	The "is isomorphic to" relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐴)    &   ⊢ 𝑊 = (Vtx‘𝐵)    &   ⊢ 𝐸 = (Edg‘𝐴)    &   ⊢ 𝐾 = (Edg‘𝐵)    ⇒   ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 ≃𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
Theorem	gricuspgr 48711*	The "is isomorphic to" relation for two simple pseudographs. This corresponds to the definition in [Bollobas] p. 3. (Contributed by AV, 1-Dec-2022.) (Proof shortened by AV, 5-May-2025.)
⊢ 𝑉 = (Vtx‘𝐴)    &   ⊢ 𝑊 = (Vtx‘𝐵)    &   ⊢ 𝐸 = (Edg‘𝐴)    &   ⊢ 𝐾 = (Edg‘𝐵)    ⇒   ⊢ ((𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph) → (𝐴 ≃𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾))))
Theorem	gricrel 48712	The "is isomorphic to" relation for graphs is a relation. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.)
⊢ Rel ≃𝑔𝑟
Theorem	gricref 48713	Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 29-Apr-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺)
Theorem	gricsym 48714	Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 3-May-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺))
Theorem	gricsymb 48715	Graph isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Proof shortened by AV, 3-May-2025.)
⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph) → (𝐴 ≃𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑔𝑟 𝐴))
Theorem	grictr 48716	Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022.) (Revised by AV, 3-May-2025.)
⊢ ((𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇) → 𝑅 ≃𝑔𝑟 𝑇)
Theorem	gricer 48717	Isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 3-May-2025.) (Proof shortened by AV, 11-Jul-2025.)
⊢ ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph
Theorem	gricen 48718	Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025.)
⊢ 𝐵 = (Vtx‘𝑅)    &   ⊢ 𝐶 = (Vtx‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶)
Theorem	opstrgric 48719	A graph represented as an extensible structure with vertices as base set and indexed edges is isomorphic to a hypergraph represented as ordered pair with the same vertices and edges. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 4-May-2025.)
⊢ 𝐺 = ⟨𝑉, 𝐸⟩    &   ⊢ 𝐻 = {⟨(Base‘ndx), 𝑉⟩, ⟨(.ef‘ndx), 𝐸⟩}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐺 ≃𝑔𝑟 𝐻)
Theorem	ushggricedg 48720	A simple hypergraph (with arbitrarily indexed edges) is isomorphic to a graph with the same vertices and the same edges, indexed by the edges themselves. (Contributed by AV, 11-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐻 = ⟨𝑉, ( I ↾ 𝐸)⟩    ⇒   ⊢ (𝐺 ∈ USHGraph → 𝐺 ≃𝑔𝑟 𝐻)
Theorem	cycldlenngric 48721*	Two simple pseudographs are not isomorphic if one has a cycle and the other has no cycle of the same length. (Contributed by AV, 6-Nov-2025.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((∃𝑝∃𝑓(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 𝑁) ∧ ¬ ∃𝑝∃𝑓(𝑓(Cycles‘𝐻)𝑝 ∧ (♯‘𝑓) = 𝑁)) → ¬ 𝐺 ≃𝑔𝑟 𝐻))
Theorem	isubgrgrim 48722*	Isomorphic subgraphs induced by subsets of vertices of two graphs. (Contributed by AV, 29-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ (((𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇) ∧ (𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊)) → ((𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr 𝑀) ↔ ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))
Theorem	uhgrimisgrgriclem 48723*	Lemma for uhgrimisgrgric 48724. (Contributed by AV, 31-May-2025.)
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))
Theorem	uhgrimisgrgric 48724	For isomorphic hypergraphs, the induced subgraph of a subset of vertices of one graph is isomorphic to the subgraph induced by the image of the subset. (Contributed by AV, 31-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁)))
Theorem	clnbgrisubgrgrim 48725*	Isomorphic subgraphs induced by closed neighborhoods of vertices of two graphs. (Contributed by AV, 29-May-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑌)    &   ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁}    &   ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀}    ⇒   ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇) → ((𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr 𝑀) ↔ ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))
Theorem	clnbgrgrimlem 48726*	Lemma for clnbgrgrim 48727: For two isomorphic hypergraphs, if there is an edge connecting the image of a vertex of the first graph with a vertex of the second graph, the vertex of the second graph is the image of a neighbor of the vertex of the first graph. (Contributed by AV, 2-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐻)    ⇒   ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌))
Theorem	clnbgrgrim 48727	Graph isomorphisms between hypergraphs map closed neighborhoods onto closed neighborhoods. (Contributed by AV, 2-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑋)))
Theorem	grimedg 48728	For two isomorphic graphs, a set of vertices is an edge in one graph iff its image by a graph isomorphism is an edge of the other graph. (Contributed by AV, 7-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉)))
Theorem	grimedgi 48729	Graph isomorphisms map edges onto the corresponding edges. (Contributed by AV, 30-Dec-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐾 ∈ 𝐼 → (𝐹 “ 𝐾) ∈ 𝐸))
21.49.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 48731 is designed for a special purpose, namely to provide a criterion for two graphs being not isomorphic (see grimgrtri 48742). 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 48731 may become obsolete.
Syntax	cgrtri 48730	Extend class notation with triangles (in a graph).
class GrTriangles
Definition	df-grtri 48731*	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 48738, and the vertices of a cycle of size 3 are a triangle in a graph, see cycl3grtri 48740. (Contributed by AV, 20-Jul-2025.)
⊢ GrTriangles = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))})
Theorem	grtriproplem 48732	Lemma for grtriprop 48734. (Contributed by AV, 23-Jul-2025.)
⊢ ((𝑓:(0..^3)–1-1-onto→{𝑥, 𝑦, 𝑧} ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝐸 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝐸 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝐸)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))
Theorem	grtri 48733*	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 48734*	The properties of a triangle. (Contributed by AV, 25-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
Theorem	grtrif1o 48735	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 48736*	A triangle in a graph. (Contributed by AV, 20-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
Theorem	grtrissvtx 48737	A triangle is a subset of the vertices (of a graph). (Contributed by AV, 26-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → 𝑇 ⊆ 𝑉)
Theorem	grtriclwlk3 48738	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 48739	Lemma for cycl3grtri 48740. (Contributed by AV, 5-Oct-2025.)
⊢ (((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ∧ (♯‘𝐹) = 3)) → ({(𝑃‘0), (𝑃‘1)} ∈ (Edg‘𝐺) ∧ {(𝑃‘0), (𝑃‘2)} ∈ (Edg‘𝐺) ∧ {(𝑃‘1), (𝑃‘2)} ∈ (Edg‘𝐺)))
Theorem	cycl3grtri 48740	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 48741	Conditions for mapping triangles onto triangles. Lemma for grimgrtri 48742 and grlimgrtri 48796. (Contributed by AV, 23-Aug-2025.)
⊢ (𝐹:𝑉–1-1→𝑊 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)) → (((𝐹‘𝑎) ∈ 𝑊 ∧ (𝐹‘𝑏) ∈ 𝑊 ∧ (𝐹‘𝑐) ∈ 𝑊) ∧ (𝐹 “ 𝑇) = {(𝐹‘𝑎), (𝐹‘𝑏), (𝐹‘𝑐)} ∧ (♯‘(𝐹 “ 𝑇)) = 3)))
Theorem	grimgrtri 48742	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 48743*	Conditions for a simple graph to contain a triangle. (Contributed by AV, 7-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑎)    ⇒   ⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
21.49.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 48744	Extend class notation with star graphs.
class StarGr
Definition	df-stgr 48745*	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 48753, (StarGr‘1) will be a single edge (graph with two vertices connected by an edge), see stgr1 48754, 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 48746*	The star graph SN. (Contributed by AV, 10-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) = {⟨(Base‘ndx), (0...𝑁)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})⟩})
Theorem	stgrvtx 48747	The vertices of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Vtx‘(StarGr‘𝑁)) = (0...𝑁))
Theorem	stgriedg 48748*	The indexed edges of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (iEdg‘(StarGr‘𝑁)) = ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}))
Theorem	stgredg 48749*	The edges of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})
Theorem	stgredgel 48750*	An edge of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (𝐸 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐸 ⊆ (0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝐸 = {0, 𝑥})))
Theorem	stgredgiun 48751*	The edges of the star graph SN as indexed union. (Contributed by AV, 29-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = ∪ 𝑥 ∈ (1...𝑁){{0, 𝑥}})
Theorem	stgrusgra 48752	The star graph SN is a simple graph. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) ∈ USGraph)
Theorem	stgr0 48753	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 48754	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 48755	The center ("internal node") of a star graph SN. (Contributed by AV, 12-Sep-2025.)
⊢ 𝐺 = (StarGr‘𝑁)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 0 ∈ 𝑉)
Theorem	stgrorder 48756	The order of a star graph SN. (Contributed by AV, 12-Sep-2025.)
⊢ 𝐺 = (StarGr‘𝑁)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (♯‘𝑉) = (𝑁 + 1))
Theorem	stgrnbgr0 48757	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 48758	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 48759	Lemma 1 for isubgr3stgr 48768. (Contributed by AV, 16-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝐹 = (𝐻 ∪ {⟨𝑋, 𝑌⟩})    ⇒   ⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐹:𝐶–1-1-onto→(𝑅 ∪ {𝑌}))
Theorem	isubgr3stgrlem2 48760*	Lemma 2 for isubgr3stgr 48768. (Contributed by AV, 16-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}))
Theorem	isubgr3stgrlem3 48761*	Lemma 3 for isubgr3stgr 48768. (Contributed by AV, 17-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0))
Theorem	isubgr3stgrlem4 48762*	Lemma 4 for isubgr3stgr 48768. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐴 = 𝑋 ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧})
Theorem	isubgr3stgrlem5 48763*	Lemma 5 for isubgr3stgr 48768. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((𝐹:𝐶⟶𝑊 ∧ 𝑌 ∈ 𝐼) → (𝐻‘𝑌) = (𝐹 “ 𝑌))
Theorem	isubgr3stgrlem6 48764*	Lemma 6 for isubgr3stgr 48768. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼⟶(Edg‘(StarGr‘𝑁)))
Theorem	isubgr3stgrlem7 48765*	Lemma 7 for isubgr3stgr 48768. (Contributed by AV, 29-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝐽) ∈ 𝐼)
Theorem	isubgr3stgrlem8 48766*	Lemma 8 for isubgr3stgr 48768. (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 48767*	Lemma 9 for isubgr3stgr 48768. (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 48768*	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.49.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 48780. This definition is according to a chat in mathoverflow (https://mathoverflow.net/questions/491133/locally-isomorphic-graphs 48780): roughly speaking, it restricts the correspondence of two graphs to their neighborhoods. Additionally, a binary relation ≃𝑙𝑔𝑟 is defined (see df-grlic 48774) 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 48809. The names and symbols are chosen analogously to group isomorphisms GrpIso (see df-gim 19335) and graph isomorphisms GraphIso (see df-grim 48671) resp. isomorphism between groups ≃𝑔 (see df-gic 19336) and isomorphism between graphs ≃𝑔𝑟 (see df-gric 48674). 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 48922. Such two graphs are the two generalized Petersen graphs G(5,K) of order 10 (see definition df-gpg 48834), which are the Petersen graph G(5,2) and the 5-prism G(5,1), see gpg5ngric 48921.
Syntax	cgrlim 48769	The class of graph local isomorphism sets.
class GraphLocIso
Syntax	cgrlic 48770	The class of the graph local isomorphism relation.
class ≃𝑙𝑔𝑟
Definition	df-grlim 48771*	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 48772	The graph local isomorphism function is a well-defined function. (Contributed by AV, 20-May-2025.)
⊢ GraphLocIso Fn (V × V)
Theorem	grlimdmrel 48773	The domain of the graph local isomorphism function is a relation. (Contributed by AV, 20-May-2025.)
⊢ Rel dom GraphLocIso
Definition	df-grlic 48774	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 48775*	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 48776*	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 48777*	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 48778	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 48779*	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 48780	An isomorphism of hypergraphs is a local isomorphism between the two graphs. (Contributed by AV, 2-Jun-2025.)
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
Theorem	uspgrlimlem1 48781*	Lemma 1 for uspgrlim 48785. (Contributed by AV, 16-Aug-2025.)
⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (𝐻 ∈ USPGraph → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}))
Theorem	uspgrlimlem2 48782*	Lemma 2 for uspgrlim 48785. (Contributed by AV, 16-Aug-2025.)
⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋)    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (𝐻 ∈ USPGraph → (◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})
Theorem	uspgrlimlem3 48783*	Lemma 3 for uspgrlim 48785. (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 48784*	Lemma 4 for uspgrlim 48785. (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 48785*	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 48776). (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 48786*	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 48787*	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 48788*	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 48789*	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 48790*	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 48791*	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 48792*	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 48793*	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 48794*	Lemma 3 for grlimgrtri 48796. (Contributed by AV, 24-Aug-2025.) (Proof shortened by AV, 27-Dec-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ 𝐼 ∧ {𝑎, 𝑐} ∈ 𝐼 ∧ {𝑏, 𝑐} ∈ 𝐼)) → ({𝑎, 𝑏} ∈ 𝐾 ∧ {𝑎, 𝑐} ∈ 𝐾 ∧ {𝑏, 𝑐} ∈ 𝐾))
Theorem	grlimgrtrilem2 48795*	Lemma 3 for grlimgrtri 48796. (Contributed by AV, 23-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁}    &   ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑎))    &   ⊢ 𝐽 = (Edg‘𝐻)    &   ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀}    ⇒   ⊢ (((𝑓:𝑁–1-1-onto→𝑀 ∧ 𝑔:𝐾–1-1-onto→𝐿) ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ 𝐾) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ 𝐽)
Theorem	grlimgrtri 48796*	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 48797	The relation "is locally isomorphic to" for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ (𝑅 GraphLocIso 𝑆) ≠ ∅)
Theorem	brgrilci 48798	Prove that two graphs are locally isomorphic by an explicit local isomorphism. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐹 ∈ (𝑅 GraphLocIso 𝑆) → 𝑅 ≃𝑙𝑔𝑟 𝑆)
Theorem	grlicrel 48799	The "is locally isomorphic to" relation for graphs is a relation. (Contributed by AV, 9-Jun-2025.)
⊢ Rel ≃𝑙𝑔𝑟
Theorem	grlicrcl 48800	Reverse closure of the "is locally isomorphic to" relation for graphs. (Contributed by AV, 9-Jun-2025.)
⊢ (𝐺 ≃𝑙𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))