P. 295 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29401-29500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	vtxdgfisnn0 29401	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 29402	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 29403	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 29404	The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 29400. (Contributed by AV, 15-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0)
Theorem	vtxdlfuhgr1v 29405*	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 29406	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 29407	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 29408	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 29409	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 29410	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 29411*	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 29412*	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 29413*	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 29414*	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 29415*	Lemma for vtxdushgrfvedg 29416 and vtxdusgrfvedg 29417. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (♯‘{𝑖 ∈ dom (iEdg‘𝐺) ∣ 𝑈 ∈ ((iEdg‘𝐺)‘𝑖)}) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	vtxdushgrfvedg 29416*	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 29417*	The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}))
Theorem	vtxduhgr0nedg 29418*	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 29419*	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 29420*	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 29421*	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 29422*	Alternate proof of vtxdusgr0edgnel 29421, not based on vtxduhgr0edgnel 29420. 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 29423	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 29424*	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 29425*	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 29426	A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 29174). (Contributed by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})    ⇒   ⊢ (𝜑 → 𝐺 ∈ USPGraph)
Theorem	1loopgredg 29427	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 29428	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 29429	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 29430	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 29431	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 29432	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 29433	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 29434	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 29435	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 29436	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 29437	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 29438	Lemma for p1evtxdeq 29439 and p1evtxdp1 29440. (Contributed by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 ((VtxDeg‘⟨𝑉, {⟨𝐾, 𝐸⟩}⟩)‘𝑈)))
Theorem	p1evtxdeq 29439	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 29440	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 29441	The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29174). (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉)
Theorem	uspgrloopvtxel 29442	A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29174). (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ (Vtx‘𝐺))
Theorem	uspgrloopiedg 29443	The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29174) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})
Theorem	uspgrloopedg 29444	The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29174) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (Edg‘𝐺) = {{𝑁}})
Theorem	uspgrloopnb0 29445	In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29174), 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 29446	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 29174), 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 29447	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 29448	A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ (Vtx‘𝐺))
Theorem	umgr2v2eiedg 29449	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 29450	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 29451	A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph)
Theorem	umgr2v2enb1 29452	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 29453	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 29454	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 29445, but degree 2, see uspgrloopvd2 29446. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 29452, but also degree 2, see umgr2v2evd2 29453. (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 29455	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 29456*	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 29457*	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 29458*	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 29459*	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 29460*	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 29461*	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 29462*	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 29463*	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 29464*	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 29465	Lemma 1 for vtxdginducedm1 29469: 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 29466*	Lemma 2 for vtxdginducedm1 29469: 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 29467*	Lemma 3 for vtxdginducedm1 29469: 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 29468*	Lemma 4 for vtxdginducedm1 29469. (Contributed by AV, 17-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (𝑊 ∈ (𝑉 ∖ {𝑁}) → (♯‘{𝑘 ∈ 𝐽 ∣ (𝐸‘𝑘) = {𝑊}}) = 0)
Theorem	vtxdginducedm1 29469*	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 29470*	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 29471*	Lemma for finsumvtxdg2sstep 29475. (Contributed by AV, 15-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (♯‘𝐸) = ((♯‘𝑃) + (♯‘𝐽)))
Theorem	finsumvtxdg2ssteplem2 29472*	Lemma for finsumvtxdg2sstep 29475. (Contributed by AV, 12-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘𝐽) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})))
Theorem	finsumvtxdg2ssteplem3 29473*	Lemma for finsumvtxdg2sstep 29475. (Contributed by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(♯‘{𝑖 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑖)}) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (♯‘𝐽))
Theorem	finsumvtxdg2ssteplem4 29474*	Lemma for finsumvtxdg2sstep 29475. (Contributed by AV, 12-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (♯‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((♯‘𝐽) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) = (2 · ((♯‘𝑃) + (♯‘𝐽))))
Theorem	finsumvtxdg2sstep 29475*	Induction step of finsumvtxdg2size 29476: In a finite pseudograph of finite size, the sum of the degrees of all vertices of the pseudograph is twice the size of the pseudograph if the sum of the degrees of all vertices of the subgraph of the pseudograph not containing one of the vertices is twice the size of the subgraph. (Contributed by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((𝑃 ∈ Fin → Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (♯‘𝑃))) → Σ𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = (2 · (♯‘𝐸))))
Theorem	finsumvtxdg2size 29476*	The sum of the degrees of all vertices of a finite pseudograph of finite size is twice the size of the pseudograph. See equation (1) in section I.1 in [Bollobas] p. 4. Here, the "proof" is simply the statement "Since each edge has two endvertices, the sum of the degrees is exactly twice the number of edges". The formal proof of this theorem (for pseudographs) is much more complicated, taking also the used auxiliary theorems into account. The proof for a (finite) simple graph (see fusgr1th 29477) would be shorter, but nevertheless still laborious. Although this theorem would hold also for infinite pseudographs and pseudographs of infinite size, the proof of this most general version (see theorem "sumvtxdg2size" below) would require many more auxiliary theorems (e.g., the extension of the sum Σ over an arbitrary set). I dedicate this theorem and its proof to Norman Megill, who deceased too early on December 9, 2021. This proof is an example for the rigor which was the main motivation for Norman Megill to invent and develop Metamath, see section 1.1.6 "Rigor" on page 19 of the Metamath book: "... it is usually assumed in mathematical literature that the person reading the proof is a mathematician familiar with the specialty being described, and that the missing steps are obvious to such a reader or at least the reader is capable of filling them in." I filled in the missing steps of Bollobas' proof as Norm would have liked it... (Contributed by Alexander van der Vekens, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))
Theorem	fusgr1th 29477*	The sum of the degrees of all vertices of a finite simple graph is twice the size of the graph. See equation (1) in section I.1 in [Bollobas] p. 4. Also known as the "First Theorem of Graph Theory" (see https://charlesreid1.com/wiki/First_Theorem_of_Graph_Theory). (Contributed by AV, 26-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))
Theorem	finsumvtxdgeven 29478*	The sum of the degrees of all vertices of a finite pseudograph of finite size is even. See equation (2) in section I.1 in [Bollobas] p. 4, where it is also called the handshaking lemma. (Contributed by AV, 22-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → 2 ∥ Σ𝑣 ∈ 𝑉 (𝐷‘𝑣))
Theorem	vtxdgoddnumeven 29479*	The number of vertices of odd degree is even in a finite pseudograph of finite size. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 22-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → 2 ∥ (♯‘{𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ (𝐷‘𝑣)}))
Theorem	fusgrvtxdgonume 29480*	The number of vertices of odd degree is even in a finite simple graph. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 27-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → 2 ∥ (♯‘{𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ (𝐷‘𝑣)}))
17.2.11  Regular graphs With df-rgr 29483 and df-rusgr 29484, k-regularity of a (simple) graph is defined as predicate RegGraph resp. RegUSGraph. Instead of defining a predicate, an alternative could have been to define a function that maps an extended nonnegative integer to the class of "graphs" in which every vertex has the extended nonnegative integer as degree: RegGraph = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘}). This function, however, would not be defined at least for 𝑘 = 0 (see rgrx0nd 29520), because {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} is not a set (see rgrprcx 29518). It is expected that this function is not defined for every 𝑘 ∈ ℕ0* (how could this be proven?).
Syntax	crgr 29481	Extend class notation to include the class of all regular graphs.
class RegGraph
Syntax	crusgr 29482	Extend class notation to include the class of all regular simple graphs.
class RegUSGraph
Definition	df-rgr 29483*	Define the "k-regular" predicate, which is true for a "graph" being k-regular: read 𝐺 RegGraph 𝐾 as "𝐺 is 𝐾-regular" or "𝐺 is a 𝐾-regular graph". Note that 𝐾 is allowed to be positive infinity (𝐾 ∈ ℕ0*), as proposed by GL. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ RegGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}
Definition	df-rusgr 29484*	Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read 𝐺 RegUSGraph 𝐾 as 𝐺 is a 𝐾-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
Theorem	isrgr 29485*	The property of a class being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGraph 𝐾 ↔ (𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
Theorem	rgrprop 29486*	The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 RegGraph 𝐾 → (𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))
Theorem	isrusgr 29487	The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾)))
Theorem	rusgrprop 29488	The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾))
Theorem	rusgrrgr 29489	A k-regular simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 RegGraph 𝐾)
Theorem	rusgrusgr 29490	A k-regular simple graph is a simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph)
Theorem	finrusgrfusgr 29491	A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph)
Theorem	isrusgr0 29492*	The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
Theorem	rusgrprop0 29493*	The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))
Theorem	usgreqdrusgr 29494*	If all vertices in a simple graph have the same degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾) → 𝐺 RegUSGraph 𝐾)
Theorem	fusgrregdegfi 29495*	In a nonempty finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.) (Revised by AV, 19-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 → 𝐾 ∈ ℕ0))
Theorem	fusgrn0eqdrusgr 29496*	If all vertices in a nonempty finite simple graph have the same (finite) degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 → 𝐺 RegUSGraph 𝐾))
Theorem	frusgrnn0 29497	In a nonempty finite k-regular simple graph, the degree of each vertex is finite. (Contributed by AV, 7-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈ ℕ0)
Theorem	0edg0rgr 29498	A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (iEdg‘𝐺) = ∅) → 𝐺 RegGraph 0)
Theorem	uhgr0edg0rgr 29499	A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ (Edg‘𝐺) = ∅) → 𝐺 RegGraph 0)
Theorem	uhgr0edg0rgrb 29500	A hypergraph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.)
⊢ (𝐺 ∈ UHGraph → (𝐺 RegGraph 0 ↔ (Edg‘𝐺) = ∅))