P. 473 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47201-47300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wtgoldbnnsum4prm 47201*	If the (weak) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes, showing that Schnirelmann's constant would be less than or equal to 4. See corollary 1.1 in [Helfgott] p. 4. (Contributed by AV, 25-Jul-2020.)
⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))
Theorem	stgoldbnnsum4prm 47202*	If the (strong) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes. (Contributed by AV, 27-Jul-2020.)
⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))
Theorem	bgoldbnnsum3prm 47203*	If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020.)
⊢ (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))
Theorem	bgoldbtbndlem1 47204	Lemma 1 for bgoldbtbnd 47208: the odd numbers between 7 and 13 (exclusive) are odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.)
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 ∈ (7[,);13)) → 𝑁 ∈ GoldbachOdd )
Theorem	bgoldbtbndlem2 47205*	Lemma 2 for bgoldbtbnd 47208. (Contributed by AV, 1-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11))    &   ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))    &   ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝐹‘0) = 7)    &   ⊢ (𝜑 → (𝐹‘1) = ;13)    &   ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))    &   ⊢ 𝑆 = (𝑋 − (𝐹‘(𝐼 − 1)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹‘𝐼)) ≤ 4) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆)))
Theorem	bgoldbtbndlem3 47206*	Lemma 3 for bgoldbtbnd 47208. (Contributed by AV, 1-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11))    &   ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))    &   ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝐹‘0) = 7)    &   ⊢ (𝜑 → (𝐹‘1) = ;13)    &   ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))    &   ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)    &   ⊢ 𝑆 = (𝑋 − (𝐹‘𝐼))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆)))
Theorem	bgoldbtbndlem4 47207*	Lemma 4 for bgoldbtbnd 47208. (Contributed by AV, 1-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11))    &   ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))    &   ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝐹‘0) = 7)    &   ⊢ (𝜑 → (𝐹‘1) = ;13)    &   ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))    &   ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)    ⇒   ⊢ (((𝜑 ∧ 𝐼 ∈ (1..^𝐷)) ∧ 𝑋 ∈ Odd ) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹‘𝐼)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑋 = ((𝑝 + 𝑞) + 𝑟))))
Theorem	bgoldbtbnd 47208*	If the binary Goldbach conjecture is valid up to an integer 𝑁, and there is a series ("ladder") of primes with a difference of at most 𝑁 up to an integer 𝑀, then the strong ternary Goldbach conjecture is valid up to 𝑀, see section 1.2.2 in [Helfgott] p. 4 with N = 4 x 10^18, taken from [OeSilva], and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11))    &   ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))    &   ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝐹‘0) = 7)    &   ⊢ (𝜑 → (𝐹‘1) = ;13)    &   ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))    &   ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd ))
Axiom	ax-bgbltosilva 47209	The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see section 2 in [OeSilva] p. 2042. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) → 𝑁 ∈ GoldbachEven )
Axiom	ax-tgoldbachgt 47210*	Temporary duplicate of tgoldbachgt 34348, provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: Odd integers greater than (;10↑;27) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of [Helfgott] p. 70 , expressed using the set 𝐺 of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021.)
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐺 = {𝑧 ∈ 𝑂 ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}    ⇒   ⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺))
Theorem	tgoldbachgtALTV 47211*	Variant of Thierry Arnoux's tgoldbachgt 34348 using the symbols Odd and GoldbachOdd: The ternary Goldbach conjecture is valid for large odd numbers (i.e. for all odd numbers greater than a fixed 𝑚). This is proven by Helfgott (see section 7.4 in [Helfgott] p. 70) for 𝑚 = 10^27. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 15-Jan-2022.)
⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ))
Theorem	bgoldbachlt 47212*	The binary Goldbach conjecture is valid for small even numbers (i.e. for all even numbers less than or equal to a fixed big 𝑚). This is verified for m = 4 x 10^18 by Oliveira e Silva, see ax-bgbltosilva 47209. (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∃𝑚 ∈ ℕ ((4 · (;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ))
Axiom	ax-hgprmladder 47213	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 47214	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 47212, ax-hgprmladder 47213 and bgoldbtbnd 47208. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd )
Theorem	tgoldbachlt 47215*	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 47214. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))
Theorem	tgoldbach 47216	The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 47215 and ax-tgoldbachgt 47210. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∀𝑛 ∈ Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOdd )
21.45.15  Graph theory (extension)
21.45.15.1  Closed neighborhood of a vertex
Syntax	cclnbgr 47217	Extend class notation with closed neighborhoods (of a vertex in a graph).
class ClNeighbVtx
Definition	df-clnbgr 47218*	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 are all vertices which are connected with this vertex by an edge and the vertex itself (in contrast to an open neighborhood, see df-nbgr 29185). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 47223. This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025.)
⊢ ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))
Theorem	clnbgrprc0 47219	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 47220	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 47221*	The closed neighborhood of a vertex 𝑉 in a graph 𝐺. (Contributed by AV, 7-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}))
Theorem	dfclnbgr2 47222*	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 47223	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	dfclnbgr3 47224*	Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval 47221). (Contributed by AV, 8-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)}))
Theorem	clnbgrnvtx0 47225	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 47226*	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 47227	Every vertex 𝐾 is a member of its closed neighborhood. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ (𝐺 ClNeighbVtx 𝐾))
Theorem	clnbgrisvtx 47228	Every member 𝑁 of the closed neighborhood of a vertex 𝐾 is a vertex. (Contributed by AV, 9-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) → 𝑁 ∈ 𝑉)
Theorem	clnbgrssvtx 47229	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 47230	The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) ≠ ∅)
Theorem	clnbupgr 47231*	The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}))
Theorem	clnbupgrel 47232	A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸)))
Theorem	clnbgr0vtx 47233	In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 ClNeighbVtx 𝐾) = ∅)
Theorem	clnbgr0edg 47234	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 47235	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	edgusgrclnbfin 47236*	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 47237	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 47238	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 47239	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.45.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 47240. The definitions for open and closed neighborhoods could be derived from such a more simple, but otherwise probably useless definition, see dfnbgr5 47245 and dfclnbgr5 47244. 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 47247. The definitions for open and closed neighborhoods could also be derived from such a definition, see dfnbgr6 47251 and dfclnbgr6 47250. 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 47240, the definition of semiopen neighborhoods is much more complex.
Theorem	dfsclnbgr2 47240*	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 47242), even only with itself (i.e., by a loop). (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)})
Theorem	sclnbgrel 47241*	Characterization of a member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑋} ⊆ 𝑒))
Theorem	sclnbgrelself 47242*	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 47243*	Every member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 is a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝑉)
Theorem	dfclnbgr5 47244*	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 47245*	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 47246*	Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁)))
Theorem	dfvopnbgr2 47247*	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 47248*	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 47249*	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 47250*	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 47251*	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 47252*	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 47253*	Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    ⇒   ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑈 ∧ 𝑈 ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁)))
21.45.15.3  Induced subgraphs
Syntax	cisubgr 47254	Extend class notation with induced subgraphs.
class ISubGr
Definition	df-isubgr 47255*	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 47256*	The subgraph induced by a subset of vertices. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) = ⟨𝑆, (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆})⟩)
Theorem	isubgriedg 47257*	The edges of an induced subgraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (iEdg‘(𝐺 ISubGr 𝑆)) = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆}))
Theorem	isubgrvtxuhgr 47258	The subgraph induced by the full set of vertices of a hypergraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr 𝑉) = ⟨𝑉, 𝐸⟩)
Theorem	isubgrvtx 47259	The vertices of an induced subgraph. (Contributed by AV, 12-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (Vtx‘(𝐺 ISubGr 𝑆)) = 𝑆)
Theorem	isubgruhgr 47260	An induced subgraph of a hypergraph is a hypergraph. (Contributed by AV, 13-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UHGraph)
Theorem	isubgrsubgr 47261	An induced subgraph of a hypergraph is a subgraph of the hypergraph. (Contributed by AV, 14-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) SubGraph 𝐺)
Theorem	isubgrupgr 47262	An induced subgraph of a pseudograph is a pseudograph. (Contributed by AV, 14-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UPGraph)
Theorem	isubgrumgr 47263	An induced subgraph of a multigraph is a multigraph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UMGraph)
Theorem	isubgrusgr 47264	An induced subgraph of a simple graph is a simple graph. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ USGraph)
Theorem	isubgr0uhgr 47265	The subgraph induced by an empty set of vertices of a hypergraph. (Contributed by AV, 13-May-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr ∅) = ⟨∅, ∅⟩)
21.45.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 47270) 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 47273) 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 19212) resp. isomorphism between groups ≃𝑔 ( see df-gic 19213). The general definition of graph isomorphisms and the relation "is isomorphic to" for graphs is specialized for simple hypergraphs (gricushgr 47291) and simple pseudographs (gricuspgr 47292). 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 47298. Finally, isomorphic graphs with different representations are studied (opstrgric 47300, ushggricedg 47301). 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 47266	Extend class notation to include the graph ispmorphisms as pair.
class GraphIsom
Syntax	cgrim 47267	Extend class notation to include the graph ispmorphisms.
class GraphIso
Syntax	cgric 47268	Extend class notation to include the "is isomorphic to" relation for graphs.
class ≃𝑔𝑟
Definition	df-grisom 47269*	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 47270. (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 47270*	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 47271	The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025.)
⊢ GraphIso Fn (V × V)
Theorem	grimdmrel 47272	The domain of the graph isomorphism function is a relation. (Contributed by AV, 28-Apr-2025.)
⊢ Rel dom GraphIso
Definition	df-gric 47273	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 47274*	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 47275*	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 47276	An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    ⇒   ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊)
Theorem	isuspgrim0lem 47277*	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 47278*	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 47279*	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 47280*	Lemma for isuspgrim 47281. (Contributed by AV, 27-Apr-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = (Vtx‘𝐻)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (Edg‘𝐻)    ⇒   ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)
Theorem	isuspgrim 47281*	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 47282	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 47283	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 47284	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 47285	The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025.)
⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ◡𝐹 ∈ (𝑇 GraphIso 𝑆)))
Theorem	grimco 47286	The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025.)
⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈))
Theorem	brgric 47287	The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.)
⊢ (𝑅 ≃𝑔𝑟 𝑆 ↔ (𝑅 GraphIso 𝑆) ≠ ∅)
Theorem	brgrici 47288	Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.)
⊢ (𝐹 ∈ (𝑅 GraphIso 𝑆) → 𝑅 ≃𝑔𝑟 𝑆)
Theorem	dfgric2 47289*	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 47290*	Implications of two graphs being isomorphic. (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	gricushgr 47291*	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 47292*	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 47293	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 47294	Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 29-Apr-2025.)
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺)
Theorem	gricsym 47295	Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 3-May-2025.)
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺))
Theorem	gricsymb 47296	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 47297	Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022.) (Revised by AV, 3-May-2025.)
⊢ ((𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇) → 𝑅 ≃𝑔𝑟 𝑇)
Theorem	gricer 47298	Isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 3-May-2025.)
⊢ ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph
Theorem	gricen 47299	Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025.)
⊢ 𝐵 = (Vtx‘𝑅)    &   ⊢ 𝐶 = (Vtx‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶)
Theorem	opstrgric 47300	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 ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐺 ≃𝑔𝑟 𝐻)