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
Axiom	ax-hgprmladder 47801	There is a partition ("ladder") of primes from 7 to 8.8 x 10^30 with parts ("rungs") having lengths of at least 4 and at most N - 4, see section 1.2.2 in [Helfgott] p. 4. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∃𝑑 ∈ (ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))
Theorem	tgblthelfgott 47802	The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in [Helfgott] p. 4, using bgoldbachlt 47800, ax-hgprmladder 47801 and bgoldbtbnd 47796. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd )
Theorem	tgoldbachlt 47803*	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 47802. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))
Theorem	tgoldbach 47804	The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 47803 and ax-tgoldbachgt 47798. (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 47805	Extend class notation with closed neighborhoods (of a vertex in a graph).
class ClNeighbVtx
Definition	df-clnbgr 47806*	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 29350). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 47811. This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025.)
⊢ ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))
Theorem	clnbgrprc0 47807	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 47808	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 47809*	The closed neighborhood of a vertex 𝑉 in a graph 𝐺. (Contributed by AV, 7-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}))
Theorem	dfclnbgr2 47810*	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 47811	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 47812	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 47813*	Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval 47809). (Contributed by AV, 8-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)}))
Theorem	clnbgrnvtx0 47814	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 47815*	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 47816	Every vertex 𝐾 is a member of its closed neighborhood. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ (𝐺 ClNeighbVtx 𝐾))
Theorem	clnbgrisvtx 47817	Every member 𝑁 of the closed neighborhood of a vertex 𝐾 is a vertex. (Contributed by AV, 9-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) → 𝑁 ∈ 𝑉)
Theorem	clnbgrssvtx 47818	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 47819	The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) ≠ ∅)
Theorem	clnbupgr 47820*	The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}))
Theorem	clnbupgrel 47821	A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸)))
Theorem	clnbgr0vtx 47822	In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 ClNeighbVtx 𝐾) = ∅)
Theorem	clnbgr0edg 47823	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 47824	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 47825	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 47826	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 47827	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 47828*	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 47829	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 47830	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 47831	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 47832. The definitions for open and closed neighborhoods could be derived from such a more simple, but otherwise probably useless definition, see dfnbgr5 47837 and dfclnbgr5 47836. 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 47839. The definitions for open and closed neighborhoods could also be derived from such a definition, see dfnbgr6 47843 and dfclnbgr6 47842. 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 47832, the definition of semiopen neighborhoods is much more complex.
Theorem	dfsclnbgr2 47832*	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 47834), even only with itself (i.e., by a loop). (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)})
Theorem	sclnbgrel 47833*	Characterization of a member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑋} ⊆ 𝑒))
Theorem	sclnbgrelself 47834*	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 47835*	Every member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 is a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝑉)
Theorem	dfclnbgr5 47836*	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 47837*	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 47838*	Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁)))
Theorem	dfvopnbgr2 47839*	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 47840*	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 47841*	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 47842*	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 47843*	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 47844*	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 47845*	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 47846	Extend class notation with induced subgraphs.
class ISubGr
Definition	df-isubgr 47847*	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 47848*	The subgraph induced by a subset of vertices. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) = ⟨𝑆, (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆})⟩)
Theorem	isubgriedg 47849*	The edges of an induced subgraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (iEdg‘(𝐺 ISubGr 𝑆)) = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆}))
Theorem	isubgrvtxuhgr 47850	The subgraph induced by the full set of vertices of a hypergraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr 𝑉) = ⟨𝑉, 𝐸⟩)
Theorem	isubgredgss 47851	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 47852	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 47853	The vertices of an induced subgraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (Vtx‘(𝐺 ISubGr 𝑆)) = 𝑆)
Theorem	isubgruhgr 47854	An induced subgraph of a hypergraph is a hypergraph. (Contributed by AV, 13-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UHGraph)
Theorem	isubgrsubgr 47855	An induced subgraph of a hypergraph is a subgraph of the hypergraph. (Contributed by AV, 14-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) SubGraph 𝐺)
Theorem	isubgrupgr 47856	An induced subgraph of a pseudograph is a pseudograph. (Contributed by AV, 14-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UPGraph)
Theorem	isubgrumgr 47857	An induced subgraph of a multigraph is a multigraph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UMGraph)
Theorem	isubgrusgr 47858	An induced subgraph of a simple graph is a simple graph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ USGraph)
Theorem	isubgr0uhgr 47859	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 47864) 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 47867) 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 19277) resp. isomorphism between groups ≃𝑔 (see df-gic 19278). The general definition of graph isomorphisms and the relation "is isomorphic to" for graphs is specialized for simple hypergraphs (gricushgr 47886) and simple pseudographs (gricuspgr 47887). 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 47893. Finally, isomorphic graphs with different representations are studied (opstrgric 47895, ushggricedg 47896). 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 47860	Extend class notation to include the graph ispmorphisms as pair.
class GraphIsom
Syntax	cgrim 47861	Extend class notation to include the graph ispmorphisms.
class GraphIso
Syntax	cgric 47862	Extend class notation to include the "is isomorphic to" relation for graphs.
class ≃𝑔𝑟
Definition	df-grisom 47863*	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 47864. (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 47864*	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 47865	The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025.)
⊢ GraphIso Fn (V × V)
Theorem	grimdmrel 47866	The domain of the graph isomorphism function is a relation. (Contributed by AV, 28-Apr-2025.)
⊢ Rel dom GraphIso
Definition	df-gric 47867	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 47868*	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 47869*	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 47870	An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
Theorem	isuspgrim0lem 47871*	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 47872*	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	uspgrimprop 47873*	An isomorphism of simple pseudographs 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. (Contributed by AV, 27-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))
Theorem	isuspgrimlem 47874*	Lemma for isuspgrim 47875. (Contributed by AV, 27-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)
Theorem	isuspgrim 47875*	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	grimidvtxedg 47876	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 47877	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 47878	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 47879	The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025.)
⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ◡𝐹 ∈ (𝑇 GraphIso 𝑆)))
Theorem	grimco 47880	The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025.)
⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈))
Theorem	brgric 47881	The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.)
⊢ (𝑅 ≃𝑔𝑟 𝑆 ↔ (𝑅 GraphIso 𝑆) ≠ ∅)
Theorem	brgrici 47882	Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.)
⊢ (𝐹 ∈ (𝑅 GraphIso 𝑆) → 𝑅 ≃𝑔𝑟 𝑆)
Theorem	gricrcl 47883	Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025.)
⊢ (𝐺 ≃𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	dfgric2 47884*	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 47885*	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 47886*	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 47887*	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 47888	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 47889	Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 29-Apr-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺)
Theorem	gricsym 47890	Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 3-May-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺))
Theorem	gricsymb 47891	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 47892	Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022.) (Revised by AV, 3-May-2025.)
⊢ ((𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇) → 𝑅 ≃𝑔𝑟 𝑇)
Theorem	gricer 47893	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 47894	Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025.)
⊢ 𝐵 = (Vtx‘𝑅)    &   ⊢ 𝐶 = (Vtx‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶)
Theorem	opstrgric 47895	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 47896	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	isubgrgrim 47897*	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 47898*	Lemma for uhgrimisgrgric 47899. (Contributed by AV, 31-May-2025.)
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))
Theorem	uhgrimisgrgric 47899	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 47900*	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→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))