P. 296 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29501-29600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cplgr2v 29501	An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by AV, 3-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 2) → (𝐺 ∈ ComplGraph ↔ 𝑉 ∈ 𝐸))
Theorem	cplgr2vpr 29502	An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) (Revised by AV, 3-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (𝐺 ∈ UHGraph ∧ 𝑉 = {𝐴, 𝐵})) → (𝐺 ∈ ComplGraph ↔ {𝐴, 𝐵} ∈ 𝐸))
Theorem	nbcplgr 29503	In a complete graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = (𝑉 ∖ {𝑁}))
Theorem	cplgr3v 29504	A pseudograph with three (different) vertices is complete iff there is an edge between each of these three vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (Vtx‘𝐺) = {𝐴, 𝐵, 𝐶}    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝐺 ∈ UPGraph ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝐺 ∈ ComplGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
Theorem	cusgr3vnbpr 29505*	The neighbors of a vertex in a simple graph with three elements are unordered pairs of the other vertices if and only if the graph is complete. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 5-Nov-2020.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ (Vtx‘𝐺) = {𝐴, 𝐵, 𝐶}    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝐺 ∈ USGraph ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝐺 ∈ ComplGraph ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(𝐺 NeighbVtx 𝑥) = {𝑦, 𝑧}))
Theorem	cplgrop 29506	A complete graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.)
⊢ (𝐺 ∈ ComplGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ ComplGraph)
Theorem	cusgrop 29507	A complete simple graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.)
⊢ (𝐺 ∈ ComplUSGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ ComplUSGraph)
Theorem	cusgrexilem1 29508*	Lemma 1 for cusgrexi 29512. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V)
Theorem	usgrexilem 29509*	Lemma for usgrexi 29510. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃):dom ( I ↾ 𝑃)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	usgrexi 29510*	An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 10-Nov-2021.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ( I ↾ 𝑃)⟩ ∈ USGraph)
Theorem	cusgrexilem2 29511*	Lemma 2 for cusgrexi 29512. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)
Theorem	cusgrexi 29512*	An arbitrary set 𝑉 regarded as set of vertices together with the set of pairs of elements of this set regarded as edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ⟨𝑉, ( I ↾ 𝑃)⟩ ∈ ComplUSGraph)
Theorem	cusgrexg 29513*	For each set there is a set of edges so that the set together with these edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.)
⊢ (𝑉 ∈ 𝑊 → ∃𝑒⟨𝑉, 𝑒⟩ ∈ ComplUSGraph)
Theorem	structtousgr 29514*	Any (extensible) structure with a base set can be made a simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021.) (Revised by AV, 17-Nov-2021.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 (Base‘𝑆) ∣ (♯‘𝑥) = 2}    &   ⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ 𝐺 = (𝑆 sSet ⟨(.ef‘ndx), ( I ↾ 𝑃)⟩)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑆)    ⇒   ⊢ (𝜑 → 𝐺 ∈ USGraph)
Theorem	structtocusgr 29515*	Any (extensible) structure with a base set can be made a complete simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021.) (Revised by AV, 17-Nov-2021.) (Proof shortened by AV, 14-Feb-2022.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 (Base‘𝑆) ∣ (♯‘𝑥) = 2}    &   ⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ 𝐺 = (𝑆 sSet ⟨(.ef‘ndx), ( I ↾ 𝑃)⟩)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑆)    ⇒   ⊢ (𝜑 → 𝐺 ∈ ComplUSGraph)
Theorem	cffldtocusgr 29516*	The field of complex numbers can be made a complete simple graph with the set of pairs of complex numbers regarded as edges. This theorem demonstrates the capabilities of the current definitions for graphs applied to extensible structures. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 17-Nov-2021.) Revise df-cnfld 21353. (Revised by GG, 31-Mar-2025.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 ℂ ∣ (♯‘𝑥) = 2}    &   ⊢ 𝐺 = (ℂfld sSet ⟨(.ef‘ndx), ( I ↾ 𝑃)⟩)    ⇒   ⊢ 𝐺 ∈ ComplUSGraph
Theorem	cusgrres 29517*	Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    &   ⊢ 𝑆 = ⟨(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)⟩    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ ComplUSGraph)
Theorem	cusgrsizeindb0 29518	Base case of the induction in cusgrsize 29523. The size of a complete simple graph with 0 vertices, actually of every null graph, is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 0) → (♯‘𝐸) = ((♯‘𝑉)C2))
Theorem	cusgrsizeindb1 29519	Base case of the induction in cusgrsize 29523. The size of a (complete) simple graph with 1 vertex is 0=((1-1)*1)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 1) → (♯‘𝐸) = ((♯‘𝑉)C2))
Theorem	cusgrsizeindslem 29520*	Lemma for cusgrsizeinds 29521. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) = ((♯‘𝑉) − 1))
Theorem	cusgrsizeinds 29521*	Part 1 of induction step in cusgrsize 29523. The size of a complete simple graph with 𝑛 vertices is (𝑛 − 1) plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹)))
Theorem	cusgrsize2inds 29522*	Induction step in cusgrsize 29523. If the size of the complete graph with 𝑛 vertices reduced by one vertex is "(𝑛 − 1) choose 2", the size of the complete graph with 𝑛 vertices is "𝑛 choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒}    ⇒   ⊢ (𝑌 ∈ ℕ0 → ((𝐺 ∈ ComplUSGraph ∧ (♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2))))
Theorem	cusgrsize 29523	The size of a finite complete simple graph with 𝑛 vertices (𝑛 ∈ ℕ0) is (𝑛C2) ("𝑛 choose 2") resp. (((𝑛 − 1)∗𝑛) / 2), see definition in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 10-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin) → (♯‘𝐸) = ((♯‘𝑉)C2))
Theorem	cusgrfilem1 29524*	Lemma 1 for cusgrfi 29527. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑃 ⊆ (Edg‘𝐺))
Theorem	cusgrfilem2 29525*	Lemma 2 for cusgrfi 29527. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    &   ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁})    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃)
Theorem	cusgrfilem3 29526*	Lemma 3 for cusgrfi 29527. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    &   ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁})    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin))
Theorem	cusgrfi 29527	If the size of a complete simple graph is finite, then its order is also finite. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝐸 ∈ Fin) → 𝑉 ∈ Fin)
Theorem	usgredgsscusgredg 29528	A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → 𝐸 ⊆ 𝐹)
Theorem	usgrsscusgr 29529*	A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → ∀𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 𝑒 = 𝑓)
Theorem	sizusglecusglem1 29530	Lemma 1 for sizusglecusg 29532. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → ( I ↾ 𝐸):𝐸–1-1→𝐹)
Theorem	sizusglecusglem2 29531	Lemma 2 for sizusglecusg 29532. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin) → 𝐸 ∈ Fin)
Theorem	sizusglecusg 29532	The size of a simple graph with 𝑛 vertices is at most the size of a complete simple graph with 𝑛 vertices (𝑛 may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐻)    &   ⊢ 𝐹 = (Edg‘𝐻)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → (♯‘𝐸) ≤ (♯‘𝐹))
Theorem	fusgrmaxsize 29533	The maximum size of a finite simple graph with 𝑛 vertices is (((𝑛 − 1)∗𝑛) / 2). See statement in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 14-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (♯‘𝐸) ≤ ((♯‘𝑉)C2))
17.2.10  Vertex degree
Syntax	cvtxdg 29534	Extend class notation with the vertex degree function.
class VtxDeg
Definition	df-vtxdg 29535*	Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain 𝑢 "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +𝑒 is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.)
⊢ VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))
Theorem	vtxdgfval 29536*	The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = (𝑢 ∈ 𝑉 ↦ ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))))
Theorem	vtxdgval 29537*	The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}})))
Theorem	vtxdgfival 29538*	The degree of a vertex for graphs of finite size. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 8-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) + (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}})))
Theorem	vtxdgop 29539	The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.)
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
Theorem	vtxdgf 29540	The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺):𝑉⟶ℕ0*)
Theorem	vtxdgelxnn0 29541	The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑋) ∈ ℕ0*)
Theorem	vtxdg0v 29542	The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 = ∅ ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdg0e 29543	The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a Königsberg graph (see also the induction steps vdegp1ai 29605, vdegp1bi 29606 and vdegp1ci 29607). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑈 ∈ 𝑉 ∧ 𝐼 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdgfisnn0 29544	The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) ∈ ℕ0)
Theorem	vtxdgfisf 29545	The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin) → (VtxDeg‘𝐺):𝑉⟶ℕ0)
Theorem	vtxdeqd 29546	Equality theorem for the vertex degree: If two graphs are structurally equal, their vertex degree functions are equal. (Contributed by AV, 26-Feb-2021.)
⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑌)    &   ⊢ (𝜑 → (Vtx‘𝐻) = (Vtx‘𝐺))    &   ⊢ (𝜑 → (iEdg‘𝐻) = (iEdg‘𝐺))    ⇒   ⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺))
Theorem	vtxduhgr0e 29547	The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 29543. (Contributed by AV, 15-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdlfuhgr1v 29548*	The degree of the vertex in a loop-free hypergraph with one vertex is 0. (Contributed by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = 0))
Theorem	vdumgr0 29549	A vertex in a multigraph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ (♯‘𝑉) = 1) → ((VtxDeg‘𝐺)‘𝑁) = 0)
Theorem	vtxdun 29550	The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 19-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → Fun 𝐽)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxdfiun 29551	The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 19-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → Fun 𝐽)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → dom 𝐽 ∈ Fin)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxduhgrun 29552	The degree of a vertex in the union of two hypergraphs on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UHGraph)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxduhgrfiun 29553	The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 7-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐽 = (iEdg‘𝐻)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉)    &   ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅)    &   ⊢ (𝜑 → 𝐺 ∈ UHGraph)    &   ⊢ (𝜑 → 𝐻 ∈ UHGraph)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽))    &   ⊢ (𝜑 → dom 𝐼 ∈ Fin)    &   ⊢ (𝜑 → dom 𝐽 ∈ Fin)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁)))
Theorem	vtxdlfgrval 29554*	The value of the vertex degree function for a loop-free graph 𝐺. (Contributed by AV, 23-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐼:𝐴⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}))
Theorem	vtxdumgrval 29555*	The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}))
Theorem	vtxdusgrval 29556*	The value of the vertex degree function for a simple graph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐴 = dom 𝐼    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}))
Theorem	vtxd0nedgb 29557*	A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝑈 ∈ 𝑉 → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖)))
Theorem	vtxdushgrfvedglem 29558*	Lemma for vtxdushgrfvedg 29559 and vtxdusgrfvedg 29560. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (♯‘{𝑖 ∈ dom (iEdg‘𝐺) ∣ 𝑈 ∈ ((iEdg‘𝐺)‘𝑖)}) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	vtxdushgrfvedg 29559*	The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = ((♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}) +𝑒 (♯‘{𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑈}})))
Theorem	vtxdusgrfvedg 29560*	The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	vtxduhgr0nedg 29561*	If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ (𝐷‘𝑈) = 0) → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸)
Theorem	vtxdumgr0nedg 29562*	If a vertex in a multigraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 15-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉 ∧ (𝐷‘𝑈) = 0) → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸)
Theorem	vtxduhgr0edgnel 29563*	A vertex in a hypergraph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 24-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒))
Theorem	vtxdusgr0edgnel 29564*	A vertex in a simple graph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒))
Theorem	vtxdusgr0edgnelALT 29565*	Alternate proof of vtxdusgr0edgnel 29564, not based on vtxduhgr0edgnel 29563. A vertex in a simple graph has degree 0 if there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒))
Theorem	vtxdgfusgrf 29566	The vertex degree function on finite simple graphs is a function from vertices to nonnegative integers. (Contributed by AV, 12-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (VtxDeg‘𝐺):𝑉⟶ℕ0)
Theorem	vtxdgfusgr 29567*	In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 12-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0)
Theorem	fusgrn0degnn0 29568*	In a nonempty, finite graph there is a vertex having a nonnegative integer as degree. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Revised by AV, 1-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → ∃𝑣 ∈ 𝑉 ∃𝑛 ∈ ℕ0 ((VtxDeg‘𝐺)‘𝑣) = 𝑛)
Theorem	1loopgruspgr 29569	A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 29318). (Contributed by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    ⇒   ⊢ (𝜑 → 𝐺 ∈ USPGraph)
Theorem	1loopgredg 29570	The set of edges in a graph (simple pseudograph) with one edge which is a loop is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    ⇒   ⊢ (𝜑 → (Edg‘𝐺) = {{𝑁}})
Theorem	1loopgrnb0 29571	In a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    ⇒   ⊢ (𝜑 → (𝐺 NeighbVtx 𝑁) = ∅)
Theorem	1loopgrvd2 29572	The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = 2)
Theorem	1loopgrvd0 29573	The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    &   ⊢ (𝜑 → 𝐾 ∈ (𝑉 ∖ {𝑁}))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐾) = 0)
Theorem	1hevtxdg0 29574	The vertex degree of vertex 𝐷 in a graph 𝐺 with only one hyperedge 𝐸 is 0 if 𝐷 is not incident with the edge 𝐸. (Contributed by AV, 2-Mar-2021.)
⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐷 ∉ 𝐸)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 0)
Theorem	1hevtxdg1 29575	The vertex degree of vertex 𝐷 in a graph 𝐺 with only one hyperedge 𝐸 (not being a loop) is 1 if 𝐷 is incident with the edge 𝐸. (Contributed by AV, 2-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.)
⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐸)    &   ⊢ (𝜑 → 2 ≤ (♯‘𝐸))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 1)
Theorem	1hegrvtxdg1 29576	The vertex degree of a graph with one hyperedge, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1)
Theorem	1hegrvtxdg1r 29577	The vertex degree of a graph with one hyperedge, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1)
Theorem	1egrvtxdg1 29578	The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1)
Theorem	1egrvtxdg1r 29579	The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1)
Theorem	1egrvtxdg0 29580	The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐷)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐷}⟩})    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 0)
Theorem	p1evtxdeqlem 29581	Lemma for p1evtxdeq 29582 and p1evtxdp1 29583. (Contributed by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 ((VtxDeg‘⟨𝑉, {⟨𝐾, 𝐸⟩}⟩)‘𝑈)))
Theorem	p1evtxdeq 29582	If an edge 𝐸 which does not contain vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is the same in both graphs. (Contributed by AV, 2-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑈 ∉ 𝐸)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = ((VtxDeg‘𝐺)‘𝑈))
Theorem	p1evtxdp1 29583	If an edge 𝐸 (not being a loop) which contains vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is increased by 1. (Contributed by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐸)    &   ⊢ (𝜑 → 2 ≤ (♯‘𝐸))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 1))
Theorem	uspgrloopvtx 29584	The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29318). (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉)
Theorem	uspgrloopvtxel 29585	A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29318). (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ (Vtx‘𝐺))
Theorem	uspgrloopiedg 29586	The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29318) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})
Theorem	uspgrloopedg 29587	The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29318) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (Edg‘𝐺) = {{𝑁}})
Theorem	uspgrloopnb0 29588	In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29318), the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = ∅)
Theorem	uspgrloopvd2 29589	The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29318), the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑁) = 2)
Theorem	umgr2v2evtx 29590	The set of vertices in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉)
Theorem	umgr2v2evtxel 29591	A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ (Vtx‘𝐺))
Theorem	umgr2v2eiedg 29592	The edge function in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩})
Theorem	umgr2v2eedg 29593	The set of edges in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Edg‘𝐺) = {{𝐴, 𝐵}})
Theorem	umgr2v2e 29594	A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph)
Theorem	umgr2v2enb1 29595	In a multigraph with two edges connecting the same two vertices, each of the vertices has one neighbor. (Contributed by AV, 18-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 NeighbVtx 𝐴) = {𝐵})
Theorem	umgr2v2evd2 29596	In a multigraph with two edges connecting the same two vertices, each of the vertices has degree 2. (Contributed by AV, 18-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((VtxDeg‘𝐺)‘𝐴) = 2)
Theorem	hashnbusgrvd 29597	In a simple graph, the number of neighbors of a vertex is the degree of this vertex. This theorem does not hold for (simple) pseudographs, because a vertex connected with itself only by a loop has no neighbors, see uspgrloopnb0 29588, but degree 2, see uspgrloopvd2 29589. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 29595, but also degree 2, see umgr2v2evd2 29596. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑈)) = ((VtxDeg‘𝐺)‘𝑈))
Theorem	usgruvtxvdb 29598	In a finite simple graph with n vertices a vertex is universal iff the vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (𝑈 ∈ (UnivVtx‘𝐺) ↔ ((VtxDeg‘𝐺)‘𝑈) = ((♯‘𝑉) − 1)))
Theorem	vdiscusgrb 29599*	A finite simple graph with n vertices is complete iff every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 22-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (𝐺 ∈ ComplUSGraph ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = ((♯‘𝑉) − 1)))
Theorem	vdiscusgr 29600*	In a finite complete simple graph with n vertices every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = ((♯‘𝑉) − 1) → 𝐺 ∈ ComplUSGraph))