P. 479 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47801-47900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tgoldbachlt 47801*	The ternary Goldbach conjecture is valid for small odd numbers (i.e. for all odd numbers less than a fixed big 𝑚 greater than 8 x 10^30). This is verified for m = 8.875694 x 10^30 by Helfgott, see tgblthelfgott 47800. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))
Theorem	tgoldbach 47802	The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 47801 and ax-tgoldbachgt 47796. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∀𝑛 ∈ Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )
21.48.15  Graph theory (extension)
21.48.15.1  Closed neighborhood of a vertex
Syntax	cclnbgr 47803	Extend class notation with closed neighborhoods (of a vertex in a graph).
class ClNeighbVtx
Definition	df-clnbgr 47804*	Define the closed neighborhood resp. the class of all neighbors of a vertex (in a graph) and the vertex itself, see definition in section I.1 of [Bollobas] p. 3. The closed neighborhood of a vertex is the set of all vertices which are connected with this vertex by an edge and the vertex itself (in contrast to an open neighborhood, see df-nbgr 29296). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 47809. This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025.)
⊢ ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))
Theorem	clnbgrprc0 47805	The closed neighborhood is empty if the graph 𝐺 or the vertex 𝑁 are proper classes. (Contributed by AV, 7-May-2025.)
⊢ (¬ (𝐺 ∈ V ∧ 𝑁 ∈ V) → (𝐺 ClNeighbVtx 𝑁) = ∅)
Theorem	clnbgrcl 47806	If a class 𝑋 has at least one element in its closed neighborhood, this class must be a vertex. (Contributed by AV, 7-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝑋) → 𝑋 ∈ 𝑉)
Theorem	clnbgrval 47807*	The closed neighborhood of a vertex 𝑉 in a graph 𝐺. (Contributed by AV, 7-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}))
Theorem	dfclnbgr2 47808*	Alternate definition of the closed neighborhood of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 7-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)}))
Theorem	dfclnbgr4 47809	Alternate definition of the closed neighborhood of a vertex as union of the vertex with its open neighborhood. (Contributed by AV, 8-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ (𝐺 NeighbVtx 𝑁)))
Theorem	elclnbgrelnbgr 47810	An element of the closed neighborhood of a vertex which is not the vertex itself is an element of the open neighborhood of the vertex. (Contributed by AV, 24-Sep-2025.)
⊢ ((𝑋 ∈ (𝐺 ClNeighbVtx 𝑁) ∧ 𝑋 ≠ 𝑁) → 𝑋 ∈ (𝐺 NeighbVtx 𝑁))
Theorem	dfclnbgr3 47811*	Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval 47807). (Contributed by AV, 8-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)}))
Theorem	clnbgrnvtx0 47812	If a class 𝑋 is not a vertex of a graph 𝐺, then it has an empty closed neighborhood in 𝐺. (Contributed by AV, 8-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑋 ∉ 𝑉 → (𝐺 ClNeighbVtx 𝑋) = ∅)
Theorem	clnbgrel 47813*	Characterization of a member 𝑁 of the closed neighborhood of a vertex 𝑋 in a graph 𝐺. (Contributed by AV, 9-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑁 = 𝑋 ∨ ∃𝑒 ∈ 𝐸 {𝑋, 𝑁} ⊆ 𝑒)))
Theorem	clnbgrvtxel 47814	Every vertex 𝐾 is a member of its closed neighborhood. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ (𝐺 ClNeighbVtx 𝐾))
Theorem	clnbgrisvtx 47815	Every member 𝑁 of the closed neighborhood of a vertex 𝐾 is a vertex. (Contributed by AV, 9-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) → 𝑁 ∈ 𝑉)
Theorem	clnbgrssvtx 47816	The closed neighborhood of a vertex 𝐾 in a graph is a subset of all vertices of the graph. (Contributed by AV, 9-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ClNeighbVtx 𝐾) ⊆ 𝑉
Theorem	clnbgrn0 47817	The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) ≠ ∅)
Theorem	clnbupgr 47818*	The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}))
Theorem	clnbupgrel 47819	A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸)))
Theorem	clnbupgreli 47820	A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 28-Dec-2025.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ (𝐺 ClNeighbVtx 𝐾)) → (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸))
Theorem	clnbgr0vtx 47821	In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 ClNeighbVtx 𝐾) = ∅)
Theorem	clnbgr0edg 47822	In an empty graph (with no edges), all closed neighborhoods consists of a single vertex. (Contributed by AV, 10-May-2025.)
⊢ (((Edg‘𝐺) = ∅ ∧ 𝐾 ∈ (Vtx‘𝐺)) → (𝐺 ClNeighbVtx 𝐾) = {𝐾})
Theorem	clnbgrsym 47823	In a graph, the closed neighborhood relation is symmetric: a vertex 𝑁 in a graph 𝐺 is a neighbor of a second vertex 𝐾 iff the second vertex 𝐾 is a neighbor of the first vertex 𝑁. (Contributed by AV, 10-May-2025.)
⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ 𝐾 ∈ (𝐺 ClNeighbVtx 𝑁))
Theorem	predgclnbgrel 47824	If a (not necessarily proper) unordered pair containing a vertex is an edge, the other vertex is in the closed neighborhood of the first vertex. (Contributed by AV, 23-Aug-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ {𝑋, 𝑁} ∈ 𝐸) → 𝑁 ∈ (𝐺 ClNeighbVtx 𝑋))
Theorem	clnbgredg 47825	A vertex connected by an edge with another vertex is a neighbor of that vertex. (Contributed by AV, 24-Aug-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾)) → 𝑌 ∈ 𝑁)
Theorem	clnbgrssedg 47826	The vertices connected by an edge are a subset of the neighborhood of each of these vertices. (Contributed by AV, 26-May-2025.) (Proof shortened by AV, 24-Aug-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾) → 𝐾 ⊆ 𝑁)
Theorem	edgusgrclnbfin 47827*	The size of the closed neighborhood of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐺 ClNeighbVtx 𝑈) ∈ Fin ↔ {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} ∈ Fin))
Theorem	clnbusgrfi 47828	The closed neighborhood of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑈) ∈ Fin)
Theorem	clnbfiusgrfi 47829	The closed neighborhood of a vertex in a finite simple graph is a finite set. (Contributed by AV, 10-May-2025.)
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ (Vtx‘𝐺)) → (𝐺 ClNeighbVtx 𝑁) ∈ Fin)
Theorem	clnbgrlevtx 47830	The size of the closed neighborhood of a vertex is at most the number of vertices of a graph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (♯‘(𝐺 ClNeighbVtx 𝑈)) ≤ (♯‘𝑉)
21.48.15.2  Semiclosed and semiopen neighborhoods (experimental) We have already definitions for open and closed neighborhoods of a vertex, which differs only in the fact that the first never contains the vertex, and the latter always contains the vertex. One of these definitions, however, cannot be simply derived from the other. This would be possible if a definition of a semiclosed neighborhood was available, see dfsclnbgr2 47831. The definitions for open and closed neighborhoods could be derived from such a more simple, but otherwise probably useless definition, see dfnbgr5 47836 and dfclnbgr5 47835. Depending on the existence of certain edges, a vertex belongs to its semiclosed neighborhood or not. An alternate approach is to introduce semiopen neighborhoods, see dfvopnbgr2 47838. The definitions for open and closed neighborhoods could also be derived from such a definition, see dfnbgr6 47842 and dfclnbgr6 47841. Like with semiclosed neighborhood, depending on the existence of certain edges, a vertex belongs to its semiopen neighborhood or not. It is unclear if either definition is/will be useful, and in contrast to dfsclnbgr2 47831, the definition of semiopen neighborhoods is much more complex.
Theorem	dfsclnbgr2 47831*	Alternate definition of the semiclosed neighborhood of a vertex breaking up the subset relationship of an unordered pair. A semiclosed neighborhood 𝑆 of a vertex 𝑁 is the set of all vertices incident with edges which join the vertex 𝑁 with a vertex. Therefore, a vertex is contained in its semiclosed neighborhood if it is connected with any vertex by an edge (see sclnbgrelself 47833), even only with itself (i.e., by a loop). (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)})
Theorem	sclnbgrel 47832*	Characterization of a member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑋} ⊆ 𝑒))
Theorem	sclnbgrelself 47833*	A vertex 𝑁 is a member of its semiclosed neighborhood iff there is an edge joining the vertex with a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑆 ↔ (𝑁 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 𝑁 ∈ 𝑒))
Theorem	sclnbgrisvtx 47834*	Every member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 is a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝑉)
Theorem	dfclnbgr5 47835*	Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiclosed neighborhood. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ 𝑆))
Theorem	dfnbgr5 47836*	Alternate definition of the (open) neighborhood of a vertex as a semiclosed neighborhood without itself. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = (𝑆 ∖ {𝑁}))
Theorem	dfnbgrss 47837*	Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁)))
Theorem	dfvopnbgr2 47838*	Alternate definition of the semiopen neighborhood of a vertex breaking up the subset relationship of an unordered pair. A semiopen neighborhood 𝑈 of a vertex 𝑁 is its open neighborhood together with itself if there is a loop at this vertex. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑈 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))})
Theorem	vopnbgrel 47839*	Characterization of a member 𝑋 of the semiopen neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 ((𝑋 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑋 ∈ 𝑒) ∨ (𝑋 = 𝑁 ∧ 𝑒 = {𝑋})))))
Theorem	vopnbgrelself 47840*	A vertex 𝑁 is a member of its semiopen neighborhood iff there is a loop joining the vertex with itself. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ 𝑈 ↔ ∃𝑒 ∈ 𝐸 𝑒 = {𝑁}))
Theorem	dfclnbgr6 47841*	Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiopen neighborhood. (Contributed by AV, 17-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ 𝑈))
Theorem	dfnbgr6 47842*	Alternate definition of the (open) neighborhood of a vertex as a difference of its semiopen neighborhood and the singleton of itself. (Contributed by AV, 17-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = (𝑈 ∖ {𝑁}))
Theorem	dfsclnbgr6 47843*	Alternate definition of a semiclosed neighborhood of a vertex as a union of a semiopen neighborhood and the vertex itself if there is a loop at this vertex. (Contributed by AV, 17-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑆 = (𝑈 ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒}))
Theorem	dfnbgrss2 47844*	Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    ⇒   ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑈 ∧ 𝑈 ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁)))
21.48.15.3  Induced subgraphs
Syntax	cisubgr 47845	Extend class notation with induced subgraphs.
class ISubGr
Definition	df-isubgr 47846*	Define the function mapping graphs and subsets of their vertices to their induced subgraphs. A subgraph induced by a subset of vertices of a graph is a subgraph of the graph which contains all edges of the graph that join vertices of the subgraph (see section I.1 in [Bollobas] p. 2 or section 1.1 in [Diestel] p. 4). Although a graph may be given in any meaningful representation, its induced subgraphs are always ordered pairs of vertices and edges. (Contributed by AV, 27-Apr-2025.)
⊢ ISubGr = (𝑔 ∈ V, 𝑣 ∈ 𝒫 (Vtx‘𝑔) ↦ ⟨𝑣, ⦋(iEdg‘𝑔) / 𝑒⦌(𝑒 ↾ {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣})⟩)
Theorem	isisubgr 47847*	The subgraph induced by a subset of vertices. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) = ⟨𝑆, (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆})⟩)
Theorem	isubgriedg 47848*	The edges of an induced subgraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (iEdg‘(𝐺 ISubGr 𝑆)) = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆}))
Theorem	isubgrvtxuhgr 47849	The subgraph induced by the full set of vertices of a hypergraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr 𝑉) = ⟨𝑉, 𝐸⟩)
Theorem	isubgredgss 47850	The edges of an induced subgraph of a graph are edges of the graph. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐻 = (𝐺 ISubGr 𝑆)    &   ⊢ 𝐼 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → 𝐼 ⊆ 𝐸)
Theorem	isubgredg 47851	An edge of an induced subgraph of a hypergraph is an edge of the hypergraph connecting vertices of the subgraph. (Contributed by AV, 24-Sep-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐻 = (𝐺 ISubGr 𝑆)    &   ⊢ 𝐼 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐾 ∈ 𝐼 ↔ (𝐾 ∈ 𝐸 ∧ 𝐾 ⊆ 𝑆)))
Theorem	isubgrvtx 47852	The vertices of an induced subgraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (Vtx‘(𝐺 ISubGr 𝑆)) = 𝑆)
Theorem	isubgruhgr 47853	An induced subgraph of a hypergraph is a hypergraph. (Contributed by AV, 13-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UHGraph)
Theorem	isubgrsubgr 47854	An induced subgraph of a hypergraph is a subgraph of the hypergraph. (Contributed by AV, 14-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) SubGraph 𝐺)
Theorem	isubgrupgr 47855	An induced subgraph of a pseudograph is a pseudograph. (Contributed by AV, 14-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UPGraph)
Theorem	isubgrumgr 47856	An induced subgraph of a multigraph is a multigraph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UMGraph)
Theorem	isubgrusgr 47857	An induced subgraph of a simple graph is a simple graph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ USGraph)
Theorem	isubgr0uhgr 47858	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 47863) 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 47866) 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 19156) resp. isomorphism between groups ≃𝑔 (see df-gic 19157). The general definition of graph isomorphisms and the relation "is isomorphic to" for graphs is specialized for simple hypergraphs (gricushgr 47902) and simple pseudographs (gricuspgr 47903). 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 47909. Finally, isomorphic graphs with different representations are studied (opstrgric 47911, ushggricedg 47912). 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 47859	Extend class notation to include the graph ispmorphisms as pair.
class GraphIsom
Syntax	cgrim 47860	Extend class notation to include the graph ispmorphisms.
class GraphIso
Syntax	cgric 47861	Extend class notation to include the "is isomorphic to" relation for graphs.
class ≃𝑔𝑟
Definition	df-grisom 47862*	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 47863. (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 47863*	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 47864	The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025.)
⊢ GraphIso Fn (V × V)
Theorem	grimdmrel 47865	The domain of the graph isomorphism function is a relation. (Contributed by AV, 28-Apr-2025.)
⊢ Rel dom GraphIso
Definition	df-gric 47866	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 47867*	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 47868*	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 47869	An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
Theorem	grimidvtxedg 47870	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 47871	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 47872	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 47873	The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025.)
⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ◡𝐹 ∈ (𝑇 GraphIso 𝑆)))
Theorem	grimco 47874	The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025.)
⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈))
Theorem	uhgrimedgi 47875	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 47876	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 47877*	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 47878*	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 47879*	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 47880*	Lemma for isuspgrim 47881. (Contributed by AV, 27-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)
Theorem	isuspgrim 47881*	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 47882*	Lemma 1 for upgrimwlk 47887 and upgrimwlklen 47888. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐹))
Theorem	upgrimwlklem2 47883*	Lemma 2 for upgrimwlk 47887. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ (𝜑 → 𝐸 ∈ Word dom 𝐽)
Theorem	upgrimwlklem3 47884*	Lemma 3 for upgrimwlk 47887. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0..^(♯‘𝐸))) → (𝐽‘(𝐸‘𝑋)) = (𝑁 “ (𝐼‘(𝐹‘𝑋))))
Theorem	upgrimwlklem4 47885*	Lemma 4 for upgrimwlk 47887. (Contributed by AV, 28-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    &   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))    ⇒   ⊢ (𝜑 → (𝑁 ∘ 𝑃):(0...(♯‘𝐸))⟶(Vtx‘𝐻))
Theorem	upgrimwlklem5 47886*	Lemma 5 for upgrimwlk 47887. (Contributed by AV, 28-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐸))) → (𝑁 “ (𝐼‘(𝐹‘𝑖))) = {((𝑁 ∘ 𝑃)‘𝑖), ((𝑁 ∘ 𝑃)‘(𝑖 + 1))})
Theorem	upgrimwlk 47887*	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 47888*	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 47889*	Lemma 1 for upgrimtrls 47891. (Contributed by AV, 29-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ dom 𝐹) → (𝑁 “ (𝐼‘(𝐹‘𝑋))) ∈ (Edg‘𝐻))
Theorem	upgrimtrlslem2 47890*	Lemma 2 for upgrimtrls 47891. (Contributed by AV, 29-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹)) → ((◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))) = (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑦)))) → 𝑥 = 𝑦))
Theorem	upgrimtrls 47891*	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 47892*	Lemma 1 for upgrimpths 47894. (Contributed by AV, 30-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → Fun ◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐹))))
Theorem	upgrimpthslem2 47893*	Lemma 2 for upgrimpths 47894. (Contributed by AV, 31-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (1..^(♯‘𝐹))) → (¬ ((𝑁 ∘ 𝑃)‘𝑋) = ((𝑁 ∘ 𝑃)‘0) ∧ ¬ ((𝑁 ∘ 𝑃)‘𝑋) = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))))
Theorem	upgrimpths 47894*	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 47895*	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 47896*	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 47897	The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.)
⊢ (𝑅 ≃𝑔𝑟 𝑆 ↔ (𝑅 GraphIso 𝑆) ≠ ∅)
Theorem	brgrici 47898	Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.)
⊢ (𝐹 ∈ (𝑅 GraphIso 𝑆) → 𝑅 ≃𝑔𝑟 𝑆)
Theorem	gricrcl 47899	Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025.)
⊢ (𝐺 ≃𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgric2 47900*	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 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))