P. 484 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48301-48400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elclnbgrelnbgr 48301	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 48302*	Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval 48298). (Contributed by AV, 8-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)}))
Theorem	clnbgrnvtx0 48303	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 48304*	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 48305	Every vertex 𝐾 is a member of its closed neighborhood. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ (𝐺 ClNeighbVtx 𝐾))
Theorem	clnbgrisvtx 48306	Every member 𝑁 of the closed neighborhood of a vertex 𝐾 is a vertex. (Contributed by AV, 9-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) → 𝑁 ∈ 𝑉)
Theorem	clnbgrssvtx 48307	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 48308	The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) ≠ ∅)
Theorem	clnbupgr 48309*	The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}))
Theorem	clnbupgrel 48310	A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸)))
Theorem	clnbupgreli 48311	A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 28-Dec-2025.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ (𝐺 ClNeighbVtx 𝐾)) → (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸))
Theorem	clnbgr0vtx 48312	In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 ClNeighbVtx 𝐾) = ∅)
Theorem	clnbgr0edg 48313	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 48314	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 48315	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 48316	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 48317	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 48318*	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 48319	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 48320	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 48321	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 48322. The definitions for open and closed neighborhoods could be derived from such a more simple, but otherwise probably useless definition, see dfnbgr5 48327 and dfclnbgr5 48326. 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 48329. The definitions for open and closed neighborhoods could also be derived from such a definition, see dfnbgr6 48333 and dfclnbgr6 48332. 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 48322, the definition of semiopen neighborhoods is much more complex.
Theorem	dfsclnbgr2 48322*	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 48324), even only with itself (i.e., by a loop). (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)})
Theorem	sclnbgrel 48323*	Characterization of a member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑋} ⊆ 𝑒))
Theorem	sclnbgrelself 48324*	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 48325*	Every member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 is a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝑉)
Theorem	dfclnbgr5 48326*	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 48327*	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 48328*	Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁)))
Theorem	dfvopnbgr2 48329*	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 48330*	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 48331*	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 48332*	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 48333*	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 48334*	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 48335*	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 48336	Extend class notation with induced subgraphs.
class ISubGr
Definition	df-isubgr 48337*	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 48338*	The subgraph induced by a subset of vertices. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) = ⟨𝑆, (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆})⟩)
Theorem	isubgriedg 48339*	The edges of an induced subgraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (iEdg‘(𝐺 ISubGr 𝑆)) = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆}))
Theorem	isubgrvtxuhgr 48340	The subgraph induced by the full set of vertices of a hypergraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr 𝑉) = ⟨𝑉, 𝐸⟩)
Theorem	isubgredgss 48341	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 48342	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 48343	The vertices of an induced subgraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (Vtx‘(𝐺 ISubGr 𝑆)) = 𝑆)
Theorem	isubgruhgr 48344	An induced subgraph of a hypergraph is a hypergraph. (Contributed by AV, 13-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UHGraph)
Theorem	isubgrsubgr 48345	An induced subgraph of a hypergraph is a subgraph of the hypergraph. (Contributed by AV, 14-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) SubGraph 𝐺)
Theorem	isubgrupgr 48346	An induced subgraph of a pseudograph is a pseudograph. (Contributed by AV, 14-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UPGraph)
Theorem	isubgrumgr 48347	An induced subgraph of a multigraph is a multigraph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UMGraph)
Theorem	isubgrusgr 48348	An induced subgraph of a simple graph is a simple graph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ USGraph)
Theorem	isubgr0uhgr 48349	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 48354) 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 48357) 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 19234) resp. isomorphism between groups ≃𝑔 (see df-gic 19235). The general definition of graph isomorphisms and the relation "is isomorphic to" for graphs is specialized for simple hypergraphs (gricushgr 48393) and simple pseudographs (gricuspgr 48394). 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 48400. Finally, isomorphic graphs with different representations are studied (opstrgric 48402, ushggricedg 48403). 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 48350	Extend class notation to include the graph ispmorphisms as pair.
class GraphIsom
Syntax	cgrim 48351	Extend class notation to include the graph ispmorphisms.
class GraphIso
Syntax	cgric 48352	Extend class notation to include the "is isomorphic to" relation for graphs.
class ≃𝑔𝑟
Definition	df-grisom 48353*	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 48354. (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 48354*	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 48355	The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025.)
⊢ GraphIso Fn (V × V)
Theorem	grimdmrel 48356	The domain of the graph isomorphism function is a relation. (Contributed by AV, 28-Apr-2025.)
⊢ Rel dom GraphIso
Definition	df-gric 48357	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 48358*	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 48359*	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 48360	An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
Theorem	grimidvtxedg 48361	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 48362	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 48363	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 48364	The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025.)
⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ◡𝐹 ∈ (𝑇 GraphIso 𝑆)))
Theorem	grimco 48365	The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025.)
⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈))
Theorem	uhgrimedgi 48366	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 48367	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 48368*	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 48369*	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 48370*	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 48371*	Lemma for isuspgrim 48372. (Contributed by AV, 27-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)
Theorem	isuspgrim 48372*	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 48373*	Lemma 1 for upgrimwlk 48378 and upgrimwlklen 48379. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ (𝜑 → (♯‘𝐸) = (♯‘𝐹))
Theorem	upgrimwlklem2 48374*	Lemma 2 for upgrimwlk 48378. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ (𝜑 → 𝐸 ∈ Word dom 𝐽)
Theorem	upgrimwlklem3 48375*	Lemma 3 for upgrimwlk 48378. (Contributed by AV, 25-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0..^(♯‘𝐸))) → (𝐽‘(𝐸‘𝑋)) = (𝑁 “ (𝐼‘(𝐹‘𝑋))))
Theorem	upgrimwlklem4 48376*	Lemma 4 for upgrimwlk 48378. (Contributed by AV, 28-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)    &   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))    ⇒   ⊢ (𝜑 → (𝑁 ∘ 𝑃):(0...(♯‘𝐸))⟶(Vtx‘𝐻))
Theorem	upgrimwlklem5 48377*	Lemma 5 for upgrimwlk 48378. (Contributed by AV, 28-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐸))) → (𝑁 “ (𝐼‘(𝐹‘𝑖))) = {((𝑁 ∘ 𝑃)‘𝑖), ((𝑁 ∘ 𝑃)‘(𝑖 + 1))})
Theorem	upgrimwlk 48378*	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 48379*	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 48380*	Lemma 1 for upgrimtrls 48382. (Contributed by AV, 29-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ dom 𝐹) → (𝑁 “ (𝐼‘(𝐹‘𝑋))) ∈ (Edg‘𝐻))
Theorem	upgrimtrlslem2 48381*	Lemma 2 for upgrimtrls 48382. (Contributed by AV, 29-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹)) → ((◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))) = (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑦)))) → 𝑥 = 𝑦))
Theorem	upgrimtrls 48382*	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 48383*	Lemma 1 for upgrimpths 48385. (Contributed by AV, 30-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → Fun ◡((𝑁 ∘ 𝑃) ↾ (1..^(♯‘𝐹))))
Theorem	upgrimpthslem2 48384*	Lemma 2 for upgrimpths 48385. (Contributed by AV, 31-Oct-2025.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ (𝜑 → 𝐺 ∈ USPGraph)    &   ⊢ (𝜑 → 𝐻 ∈ USPGraph)    &   ⊢ (𝜑 → 𝑁 ∈ (𝐺 GraphIso 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ dom 𝐹 ↦ (◡𝐽‘(𝑁 “ (𝐼‘(𝐹‘𝑥)))))    &   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (1..^(♯‘𝐹))) → (¬ ((𝑁 ∘ 𝑃)‘𝑋) = ((𝑁 ∘ 𝑃)‘0) ∧ ¬ ((𝑁 ∘ 𝑃)‘𝑋) = ((𝑁 ∘ 𝑃)‘(♯‘𝐹))))
Theorem	upgrimpths 48385*	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 48386*	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 48387*	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 48388	The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.)
⊢ (𝑅 ≃𝑔𝑟 𝑆 ↔ (𝑅 GraphIso 𝑆) ≠ ∅)
Theorem	brgrici 48389	Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.)
⊢ (𝐹 ∈ (𝑅 GraphIso 𝑆) → 𝑅 ≃𝑔𝑟 𝑆)
Theorem	gricrcl 48390	Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025.)
⊢ (𝐺 ≃𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgric2 48391*	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 48392*	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 48393*	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 48394*	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 48395	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 48396	Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 29-Apr-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺)
Theorem	gricsym 48397	Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 3-May-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺))
Theorem	gricsymb 48398	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 48399	Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022.) (Revised by AV, 3-May-2025.)
⊢ ((𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇) → 𝑅 ≃𝑔𝑟 𝑇)
Theorem	gricer 48400	Isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 3-May-2025.) (Proof shortened by AV, 11-Jul-2025.)
⊢ ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph