P. 265 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26401-26500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cusgrsizeindb0 26401	Base case of the induction in cusgrsize 26406. 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 26402	Base case of the induction in cusgrsize 26406. 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 26403*	Lemma for cusgrsizeinds 26404. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) = ((#‘𝑉) − 1))
Theorem	cusgrsizeinds 26404*	Part 1 of induction step in cusgrsize 26406. 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 26405*	Induction step in cusgrsize 26406. 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 26406	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 26407*	Lemma 1 for cusgrfi 26410. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑃 ⊆ (Edg‘𝐺))
Theorem	cusgrfilem2 26408*	Lemma 2 for cusgrfi 26410. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    &   ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁})    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃)
Theorem	cusgrfilem3 26409*	Lemma 3 for cusgrfi 26410. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})}    &   ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁})    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin))
Theorem	cusgrfi 26410	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 26411	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 26412*	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 26413	Lemma 1 for sizusglecusg 26415. (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 26414	Lemma 2 for sizusglecusg 26415. (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 26415	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 26416	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))
16.2.10  Vertex degree
Syntax	cvtxdg 26417	Extend class notation with the vertex degree function.
class VtxDeg
Definition	df-vtxdg 26418*	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 26419*	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 26420*	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 26421*	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 26422	The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.)
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
Theorem	vtxdgf 26423	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 26424	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 26425	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 26426	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 26488, vdegp1bi 26489 and vdegp1ci 26490). (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 26427	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 26428	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 26429	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 26430	The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 26426. (Contributed by AV, 15-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdlfuhgr1v 26431*	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 26432	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 26433	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 26434	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 26435	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 26436	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 26437*	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 26438*	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 26439*	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 26440*	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 26441*	Lemma for vtxdushgrfvedg 26442 and vtxdusgrfvedg 26443. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (#‘{𝑖 ∈ dom (iEdg‘𝐺) ∣ 𝑈 ∈ ((iEdg‘𝐺)‘𝑖)}) = (#‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	vtxdushgrfvedg 26442*	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 26443*	The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (#‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	vtxduhgr0nedg 26444*	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 26445*	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 26446*	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 26447*	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 26448*	Alternate proof of vtxdusgr0edgnel 26447, not based on vtxduhgr0edgnel 26446. 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 26449	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 26450*	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 26451*	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 26452	A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 26186). (Contributed by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    ⇒   ⊢ (𝜑 → 𝐺 ∈ USPGraph)
Theorem	1loopgredg 26453	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 26454	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 26455	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 26456	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 26457	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 26458	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 26459	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 26460	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 26461	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 26462	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 26463	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 26464	Lemma for p1evtxdeq 26465 and p1evtxdp1 26466. (Contributed by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 ((VtxDeg‘⟨𝑉, {⟨𝐾, 𝐸⟩}⟩)‘𝑈)))
Theorem	p1evtxdeq 26465	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 26466	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 26467	The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186). (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉)
Theorem	uspgrloopvtxel 26468	A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186). (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ (Vtx‘𝐺))
Theorem	uspgrloopiedg 26469	The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})
Theorem	uspgrloopedg 26470	The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (Edg‘𝐺) = {{𝑁}})
Theorem	uspgrloopnb0 26471	In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186), 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 26472	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 26186), 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 26473	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 26474	A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ (Vtx‘𝐺))
Theorem	umgr2v2eiedg 26475	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 26476	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 26477	A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph)
Theorem	umgr2v2enb1 26478	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 26479	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 26480	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 26471, but degree 2, see uspgrloopvd2 26472. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 26478, but also degree 2, see umgr2v2evd2 26479. (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 26481	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 26482*	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 26483*	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))
Theorem	vtxdusgradjvtx 26484*	The degree of a vertex in a simple graph is the number of vertices adjacent to this vertex. (Contributed by Alexander van der Vekens, 9-Jul-2018.) (Revised by AV, 23-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = (#‘{𝑣 ∈ 𝑉 ∣ {𝑈, 𝑣} ∈ 𝐸}))
Theorem	usgrvd0nedg 26485*	If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 16-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (((VtxDeg‘𝐺)‘𝑈) = 0 → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸))
Theorem	uhgrvd00 26486*	If every vertex in a hypergraph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → 𝐸 = ∅))
Theorem	usgrvd00 26487*	If every vertex in a simple graph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → 𝐸 = ∅))
Theorem	vdegp1ai 26488*	The induction step for a vertex degree calculation. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑌} to the edge set, where 𝑋 ≠ 𝑈 ≠ 𝑌, yields degree 𝑃 as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 ∈ 𝑉    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}    &   ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃    &   ⊢ (Vtx‘𝐹) = 𝑉    &   ⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑋 ≠ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝑌 ≠ 𝑈    &   ⊢ (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑋, 𝑌}”⟩)    ⇒   ⊢ ((VtxDeg‘𝐹)‘𝑈) = 𝑃
Theorem	vdegp1bi 26489*	The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑈, 𝑋} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 ∈ 𝑉    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}    &   ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃    &   ⊢ (Vtx‘𝐹) = 𝑉    &   ⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑋 ≠ 𝑈    &   ⊢ (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑈, 𝑋}”⟩)    ⇒   ⊢ ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1)
Theorem	vdegp1ci 26490*	The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑈} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 ∈ 𝑉    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}    &   ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃    &   ⊢ (Vtx‘𝐹) = 𝑉    &   ⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑋 ≠ 𝑈    &   ⊢ (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑋, 𝑈}”⟩)    ⇒   ⊢ ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1)
Theorem	vtxdginducedm1lem1 26491	Lemma 1 for vtxdginducedm1 26495: the edge function in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    ⇒   ⊢ (iEdg‘𝑆) = 𝑃
Theorem	vtxdginducedm1lem2 26492*	Lemma 2 for vtxdginducedm1 26495: the domain of the edge function in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    ⇒   ⊢ dom (iEdg‘𝑆) = 𝐼
Theorem	vtxdginducedm1lem3 26493*	Lemma 3 for vtxdginducedm1 26495: an edge in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    ⇒   ⊢ (𝐻 ∈ 𝐼 → ((iEdg‘𝑆)‘𝐻) = (𝐸‘𝐻))
Theorem	vtxdginducedm1lem4 26494*	Lemma 4 for vtxdginducedm1 26495. (Contributed by AV, 17-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (𝑊 ∈ (𝑉 ∖ {𝑁}) → (#‘{𝑘 ∈ 𝐽 ∣ (𝐸‘𝑘) = {𝑊}}) = 0)
Theorem	vtxdginducedm1 26495*	The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 17-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) +𝑒 (#‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)}))
Theorem	vtxdginducedm1fi 26496*	The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 of finite size obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 18-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (𝐸 ∈ Fin → ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) + (#‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)})))
Theorem	finsumvtxdg2ssteplem1 26497*	Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 15-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (#‘𝐸) = ((#‘𝑃) + (#‘𝐽)))
Theorem	finsumvtxdg2ssteplem2 26498*	Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 12-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((VtxDeg‘𝐺)‘𝑁) = ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})))
Theorem	finsumvtxdg2ssteplem3 26499*	Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑖)}) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (#‘𝐽))
Theorem	finsumvtxdg2ssteplem4 26500*	Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 12-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) = (2 · ((#‘𝑃) + (#‘𝐽))))