P. 480 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47901-48000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isubgrumgr 47901	An induced subgraph of a multigraph is a multigraph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UMGraph)
Theorem	isubgrusgr 47902	An induced subgraph of a simple graph is a simple graph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ USGraph)
Theorem	isubgr0uhgr 47903	The subgraph induced by an empty set of vertices of a hypergraph. (Contributed by AV, 13-May-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr ∅) = ⟨∅, ∅⟩)
21.48.15.4  Isomorphisms of graphs This section is about isomorphisms of graphs, whereby the term "isomorphism" is used in both of its meanings (according to the Meriam-Webster dictionary, see https://www.merriam-webster.com/dictionary/isomorphism): "1: the quality or state of being isomorphic." and "2: a one-to-one correspondence between two mathematical sets". At first, an operation GraphIso is defined (see df-grim 47908) which provides the graph isomorphisms (as "one-to-one correspondence") between two given graphs. This definition, however, is applicable for any two sets, but is meaningful only if these sets have "vertices" and "edges". Afterwards, a binary relation ≃𝑔𝑟 is defined (see df-gric 47911) which is true for two graphs iff there is a graph isomorphisms between these graphs. Then these graphs are called "isomorphic". Therefore, this relation is also called "is isomorphic to" relation. More formally, 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃𝑓𝑓 ∈ (𝐴 GraphIso 𝐵) resp. 𝐴 ≃𝑔𝑟 𝐵 ↔ (𝐴 GraphIso 𝐵) ≠ ∅. Notice that there can be multiple isomorphisms between two graphs. For example, let ⟨{𝐴, 𝐵}, {{𝐴, 𝐵}}⟩ and ⟨{{𝑀, 𝑁}, {{𝑀, 𝑁}}⟩ be two graphs with two vertices and one edge, then 𝐴 ↦ 𝑀, 𝐵 ↦ 𝑁 and 𝐴 ↦ 𝑁, 𝐵 ↦ 𝑀 are two different isomorphisms between these graphs. The names and symbols are chosen analogously to group isomorphisms GrpIso (see df-gim 19169) resp. isomorphism between groups ≃𝑔 (see df-gic 19170). The general definition of graph isomorphisms and the relation "is isomorphic to" for graphs is specialized for simple hypergraphs (gricushgr 47947) and simple pseudographs (gricuspgr 47948). The latter corresponds to the definition in [Bollobas] p. 3. It is shown that the relation "is isomorphic to" for graphs is an equivalence relation, see gricer 47954. Finally, isomorphic graphs with different representations are studied (opstrgric 47956, ushggricedg 47957). Another approach could be to define a category of graphs (there are maybe multiple ones), where graph morphisms are couples consisting of a function on vertices and a function on edges with required compatibilities, as used in the definition of GraphIso. And then, a graph isomorphism is defined as an isomorphism in the category of graphs (something like "GraphIsom = ( Iso ` GraphCat )" ). Then general category theory theorems could be used, e.g., to show that graph isomorphism is an equivalence relation.
Syntax	cgrisom 47904	Extend class notation to include the graph ispmorphisms as pair.
class GraphIsom
Syntax	cgrim 47905	Extend class notation to include the graph ispmorphisms.
class GraphIso
Syntax	cgric 47906	Extend class notation to include the "is isomorphic to" relation for graphs.
class ≃𝑔𝑟
Definition	df-grisom 47907*	Define the class of all isomorphisms between two graphs. In contrast to (𝐹 GraphIso 𝐻), which is a set of functions between the vertices, (𝐹 GraphIsom 𝐻) is a set of pairs of functions: a function between the vertices, and a function between the (indices of the) edges. It is not clear if such a definition is useful. In the definition by [Diestel] p. 3, for example, the bijection between the vertices is called an isomorphism, as formalized in df-grim 47908. (Contributed by AV, 11-Dec-2022.) (New usage is discouraged.)
⊢ GraphIsom = (𝑥 ∈ V, 𝑦 ∈ V ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))})
Definition	df-grim 47908*	An isomorphism between two graphs is a bijection between the sets of vertices of the two graphs that preserves adjacency, see definition in [Diestel] p. 3. (Contributed by AV, 19-Apr-2025.)
⊢ GraphIso = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∃𝑗[(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))))})
Theorem	grimfn 47909	The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025.)
⊢ GraphIso Fn (V × V)
Theorem	grimdmrel 47910	The domain of the graph isomorphism function is a relation. (Contributed by AV, 28-Apr-2025.)
⊢ Rel dom GraphIso
Definition	df-gric 47911	Two graphs are said to be isomorphic iff they are connected by at least one isomorphism, see definition in [Diestel] p. 3 and definition in [Bollobas] p. 3. Isomorphic graphs share all global graph properties like order and size. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 19-Apr-2025.)
⊢ ≃𝑔𝑟 = (◡ GraphIso “ (V ∖ 1o))
Theorem	isgrim 47912*	An isomorphism of graphs is a bijection between their vertices that preserves adjacency. (Contributed by AV, 19-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (iEdg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom 𝐸–1-1-onto→dom 𝐷 ∧ ∀𝑖 ∈ dom 𝐸(𝐷‘(𝑗‘𝑖)) = (𝐹 “ (𝐸‘𝑖))))))
Theorem	grimprop 47913*	Properties of an isomorphism of graphs. (Contributed by AV, 29-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (iEdg‘𝐻)    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom 𝐸–1-1-onto→dom 𝐷 ∧ ∀𝑖 ∈ dom 𝐸(𝐷‘(𝑗‘𝑖)) = (𝐹 “ (𝐸‘𝑖)))))
Theorem	grimf1o 47914	An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
Theorem	grimidvtxedg 47915	The identity relation restricted to the set of vertices of a graph is a graph isomorphism between the graph and a graph with the same vertices and edges. (Contributed by AV, 4-May-2025.)
⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝐺) = (Vtx‘𝐻))    &   ⊢ (𝜑 → (iEdg‘𝐺) = (iEdg‘𝐻))    ⇒   ⊢ (𝜑 → ( I ↾ (Vtx‘𝐺)) ∈ (𝐺 GraphIso 𝐻))
Theorem	grimid 47916	The identity relation restricted to the set of vertices of a graph is a graph isomorphism between the graph and itself. (Contributed by AV, 29-Apr-2025.) (Prove shortened by AV, 5-May-2025.)
⊢ (𝐺 ∈ UHGraph → ( I ↾ (Vtx‘𝐺)) ∈ (𝐺 GraphIso 𝐺))
Theorem	grimuhgr 47917	If there is a graph isomorphism between a hypergraph and a class with an edge function, the class is also a hypergraph. (Contributed by AV, 2-May-2025.)
⊢ ((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇) ∧ Fun (iEdg‘𝑇)) → 𝑇 ∈ UHGraph)
Theorem	grimcnv 47918	The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025.)
⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ◡𝐹 ∈ (𝑇 GraphIso 𝑆)))
Theorem	grimco 47919	The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025.)
⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈))
Theorem	uhgrimedgi 47920	An isomorphism between graphs preserves edges, i.e. if there is an edge in one graph connecting vertices then there is an edge in the other graph connecting the corresponding vertices. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝐾 ∈ 𝐸)) → (𝐹 “ 𝐾) ∈ 𝐷)
Theorem	uhgrimedg 47921	An isomorphism between graphs preserves edges, i.e. there is an edge in one graph connecting vertices iff there is an edge in the other graph connecting the corresponding vertices. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝐾 ⊆ (Vtx‘𝐺)) → (𝐾 ∈ 𝐸 ↔ (𝐹 “ 𝐾) ∈ 𝐷))
Theorem	uhgrimprop 47922*	An isomorphism between hypergraphs is a bijection between their vertices that preserves adjacency for simple edges, i.e. there is a simple edge in one graph connecting one or two vertices iff there is a simple edge in the other graph connecting the vertices which are the images of the vertices. (Contributed by AV, 27-Apr-2025.) (Revised by AV, 25-Oct-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)))
Theorem	isuspgrim0lem 47923*	An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑀 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))    &   ⊢ 𝑁 = (𝑥 ∈ dom 𝐼 ↦ (◡𝐽‘(𝑀‘(𝐼‘𝑥))))    ⇒   ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖))))
Theorem	isuspgrim0 47924*	An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)))
Theorem	isuspgrimlem 47925*	Lemma for isuspgrim 47926. (Contributed by AV, 27-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)
Theorem	isuspgrim 47926*	A class is an isomorphism of simple pseudographs iff it is a bijection between their vertices that preserves adjacency, i.e. there is an edge in one graph connecting one or two vertices iff there is an edge in the other graph connecting the vertices which are the images of the vertices. This corresponds to the formal definition in [Bollobas] p. 3 and the definition in [Diestel] p. 3. (Contributed by AV, 27-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))
Theorem	upgrimwlklem1 47927*	Lemma 1 for upgrimwlk 47932 and upgrimwlklen 47933. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐹))
Theorem	upgrimwlklem2 47928*	Lemma 2 for upgrimwlk 47932. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ (𝜑 → 𝐸 ∈ Word dom 𝐽)
Theorem	upgrimwlklem3 47929*	Lemma 3 for upgrimwlk 47932. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0..^(♯‘𝐸))) → (𝐽‘(𝐸‘𝑋)) = (𝑁 “ (𝐼‘(𝐹‘𝑋))))
Theorem	upgrimwlklem4 47930*	Lemma 4 for upgrimwlk 47932. (Contributed by AV, 28-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    &   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))    ⇒   ⊢ (𝜑 → (𝑁 ∘ 𝑃):(0...(♯‘𝐸))⟶(Vtx‘𝐻))
Theorem	upgrimwlklem5 47931*	Lemma 5 for upgrimwlk 47932. (Contributed by AV, 28-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐸))) → (𝑁 “ (𝐼‘(𝐹‘𝑖))) = {((𝑁 ∘ 𝑃)‘𝑖), ((𝑁 ∘ 𝑃)‘(𝑖 + 1))})
Theorem	upgrimwlk 47932*	Graph isomorphisms between simple pseudographs map walks onto walks. (Contributed by AV, 28-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐸(Walks‘𝐻)(𝑁 ∘ 𝑃))
Theorem	upgrimwlklen 47933*	Graph isomorphisms between simple pseudographs map walks onto walks of the same length. (Contributed by AV, 6-Nov-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → (𝐸(Walks‘𝐻)(𝑁 ∘ 𝑃) ∧ (♯‘𝐸) = (♯‘𝐹)))
Theorem	upgrimtrlslem1 47934*	Lemma 1 for upgrimtrls 47936. (Contributed by AV, 29-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ dom 𝐹) → (𝑁 “ (𝐼‘(𝐹‘𝑋))) ∈ (Edg‘𝐻))
Theorem	upgrimtrlslem2 47935*	Lemma 2 for upgrimtrls 47936. (Contributed by AV, 29-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹)) → ((◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))) = (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑦)))) → 𝑥 = 𝑦))
Theorem	upgrimtrls 47936*	Graph isomorphisms between simple pseudographs map trails onto trails. (Contributed by AV, 29-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐸(Trails‘𝐻)(𝑁 ∘ 𝑃))
Theorem	upgrimpthslem1 47937*	Lemma 1 for upgrimpths 47939. (Contributed by AV, 30-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → Fun ◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐹))))
Theorem	upgrimpthslem2 47938*	Lemma 2 for upgrimpths 47939. (Contributed by AV, 31-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (1..^(♯‘𝐹))) → (¬ ((𝑁 ∘ 𝑃)‘𝑋) = ((𝑁 ∘ 𝑃)‘0) ∧ ¬ ((𝑁 ∘ 𝑃)‘𝑋) = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))))
Theorem	upgrimpths 47939*	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 47940*	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 47941*	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 47942	The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.)
⊢ (𝑅 ≃𝑔𝑟 𝑆 ↔ (𝑅 GraphIso 𝑆) ≠ ∅)
Theorem	brgrici 47943	Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.)
⊢ (𝐹 ∈ (𝑅 GraphIso 𝑆) → 𝑅 ≃𝑔𝑟 𝑆)
Theorem	gricrcl 47944	Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025.)
⊢ (𝐺 ≃𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgric2 47945*	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 47946*	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 47947*	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 47948*	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 47949	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 47950	Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 29-Apr-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺)
Theorem	gricsym 47951	Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 3-May-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺))
Theorem	gricsymb 47952	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 47953	Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022.) (Revised by AV, 3-May-2025.)
⊢ ((𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇) → 𝑅 ≃𝑔𝑟 𝑇)
Theorem	gricer 47954	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 47955	Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025.)
⊢ 𝐵 = (Vtx‘𝑅)    &   ⊢ 𝐶 = (Vtx‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶)
Theorem	opstrgric 47956	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 47957	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 47958*	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 47959*	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 47960*	Lemma for uhgrimisgrgric 47961. (Contributed by AV, 31-May-2025.)
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))
Theorem	uhgrimisgrgric 47961	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 47962*	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 47963*	Lemma for clnbgrgrim 47964: 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 47964	Graph isomorphisms between hypergraphs map closed neighborhoods onto closed neighborhoods. (Contributed by AV, 2-Jun-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑋)))
Theorem	grimedg 47965	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 47966	Graph isomorphisms map edges onto the corresponding edges. (Contributed by AV, 30-Dec-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (Edg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐾 ∈ 𝐼 → (𝐹 “ 𝐾) ∈ 𝐸))
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 47968 is designed for a special purpose, namely to provide a criterion for two graphs being not isomorphic (see grimgrtri 47979). 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 47968 may become obsolete.
Syntax	cgrtri 47967	Extend class notation with triangles (in a graph).
class GrTriangles
Definition	df-grtri 47968*	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 47975, and the vertices of a cycle of size 3 are a triangle in a graph, see cycl3grtri 47977. (Contributed by AV, 20-Jul-2025.)
⊢ GrTriangles = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))})
Theorem	grtriproplem 47969	Lemma for grtriprop 47971. (Contributed by AV, 23-Jul-2025.)
⊢ ((𝑓:(0..^3)–1-1-onto→{𝑥, 𝑦, 𝑧} ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝐸 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝐸 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝐸)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))
Theorem	grtri 47970*	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 47971*	The properties of a triangle. (Contributed by AV, 25-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
Theorem	grtrif1o 47972	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 47973*	A triangle in a graph. (Contributed by AV, 20-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
Theorem	grtrissvtx 47974	A triangle is a subset of the vertices (of a graph). (Contributed by AV, 26-Jul-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → 𝑇 ⊆ 𝑉)
Theorem	grtriclwlk3 47975	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 47976	Lemma for cycl3grtri 47977. (Contributed by AV, 5-Oct-2025.)
⊢ (((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ∧ (♯‘𝐹) = 3)) → ({(𝑃‘0), (𝑃‘1)} ∈ (Edg‘𝐺) ∧ {(𝑃‘0), (𝑃‘2)} ∈ (Edg‘𝐺) ∧ {(𝑃‘1), (𝑃‘2)} ∈ (Edg‘𝐺)))
Theorem	cycl3grtri 47977	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 47978	Conditions for mapping triangles onto triangles. Lemma for grimgrtri 47979 and grlimgrtri 48033. (Contributed by AV, 23-Aug-2025.)
⊢ (𝐹:𝑉–1-1→𝑊 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)) → (((𝐹‘𝑎) ∈ 𝑊 ∧ (𝐹‘𝑏) ∈ 𝑊 ∧ (𝐹‘𝑐) ∈ 𝑊) ∧ (𝐹 “ 𝑇) = {(𝐹‘𝑎), (𝐹‘𝑏), (𝐹‘𝑐)} ∧ (♯‘(𝐹 “ 𝑇)) = 3)))
Theorem	grimgrtri 47979	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 47980*	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 47981	Extend class notation with star graphs.
class StarGr
Definition	df-stgr 47982*	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 47990, (StarGr‘1) will be a single edge (graph with two vertices connected by an edge), see stgr1 47991, 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 47983*	The star graph SN. (Contributed by AV, 10-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) = {⟨(Base‘ndx), (0...𝑁)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})⟩})
Theorem	stgrvtx 47984	The vertices of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Vtx‘(StarGr‘𝑁)) = (0...𝑁))
Theorem	stgriedg 47985*	The indexed edges of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (iEdg‘(StarGr‘𝑁)) = ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}))
Theorem	stgredg 47986*	The edges of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})
Theorem	stgredgel 47987*	An edge of the star graph SN. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (𝐸 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐸 ⊆ (0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝐸 = {0, 𝑥})))
Theorem	stgredgiun 47988*	The edges of the star graph SN as indexed union. (Contributed by AV, 29-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = ∪ 𝑥 ∈ (1...𝑁){{0, 𝑥}})
Theorem	stgrusgra 47989	The star graph SN is a simple graph. (Contributed by AV, 11-Sep-2025.)
⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) ∈ USGraph)
Theorem	stgr0 47990	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 47991	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 47992	The center ("internal node") of a star graph SN. (Contributed by AV, 12-Sep-2025.)
⊢ 𝐺 = (StarGr‘𝑁)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 0 ∈ 𝑉)
Theorem	stgrorder 47993	The order of a star graph SN. (Contributed by AV, 12-Sep-2025.)
⊢ 𝐺 = (StarGr‘𝑁)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (♯‘𝑉) = (𝑁 + 1))
Theorem	stgrnbgr0 47994	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 47995	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 47996	Lemma 1 for isubgr3stgr 48005. (Contributed by AV, 16-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝐹 = (𝐻 ∪ {⟨𝑋, 𝑌⟩})    ⇒   ⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐹:𝐶–1-1-onto→(𝑅 ∪ {𝑌}))
Theorem	isubgr3stgrlem2 47997*	Lemma 2 for isubgr3stgr 48005. (Contributed by AV, 16-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}))
Theorem	isubgr3stgrlem3 47998*	Lemma 3 for isubgr3stgr 48005. (Contributed by AV, 17-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0))
Theorem	isubgr3stgrlem4 47999*	Lemma 4 for isubgr3stgr 48005. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐴 = 𝑋 ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧})
Theorem	isubgr3stgrlem5 48000*	Lemma 5 for isubgr3stgr 48005. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑆 = (StarGr‘𝑁)    &   ⊢ 𝑊 = (Vtx‘𝑆)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))    &   ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))    ⇒   ⊢ ((𝐹:𝐶⟶𝑊 ∧ 𝑌 ∈ 𝐼) → (𝐻‘𝑌) = (𝐹 “ 𝑌))