Definition df-vtxdg 27736

Description: 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.)

Assertion

Ref	Expression
df-vtxdg	⊢ VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))

Distinct variable group:   𝑒,𝑔,𝑢,𝑣,𝑥

Detailed syntax breakdown of Definition df-vtxdg

Step	Hyp	Ref	Expression
1		cvtxdg 27735	. 2 class VtxDeg
2		vg	. . 3 setvar 𝑔
3		cvv 3422	. . 3 class V
4		vv	. . . 4 setvar 𝑣
5	2	cv 1538	. . . . 5 class 𝑔
6		cvtx 27269	. . . . 5 class Vtx
7	5, 6	cfv 6418	. . . 4 class (Vtx‘𝑔)
8		ve	. . . . 5 setvar 𝑒
9		ciedg 27270	. . . . . 6 class iEdg
10	5, 9	cfv 6418	. . . . 5 class (iEdg‘𝑔)
11		vu	. . . . . 6 setvar 𝑢
12	4	cv 1538	. . . . . 6 class 𝑣
13	11	cv 1538	. . . . . . . . . 10 class 𝑢
14		vx	. . . . . . . . . . . 12 setvar 𝑥
15	14	cv 1538	. . . . . . . . . . 11 class 𝑥
16	8	cv 1538	. . . . . . . . . . 11 class 𝑒
17	15, 16	cfv 6418	. . . . . . . . . 10 class (𝑒‘𝑥)
18	13, 17	wcel 2108	. . . . . . . . 9 wff 𝑢 ∈ (𝑒‘𝑥)
19	16	cdm 5580	. . . . . . . . 9 class dom 𝑒
20	18, 14, 19	crab 3067	. . . . . . . 8 class {𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}
21		chash 13972	. . . . . . . 8 class ♯
22	20, 21	cfv 6418	. . . . . . 7 class (♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)})
23	13	csn 4558	. . . . . . . . . 10 class {𝑢}
24	17, 23	wceq 1539	. . . . . . . . 9 wff (𝑒‘𝑥) = {𝑢}
25	24, 14, 19	crab 3067	. . . . . . . 8 class {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}
26	25, 21	cfv 6418	. . . . . . 7 class (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})
27		cxad 12775	. . . . . . 7 class +𝑒
28	22, 26, 27	co 7255	. . . . . 6 class ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))
29	11, 12, 28	cmpt 5153	. . . . 5 class (𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))
30	8, 10, 29	csb 3828	. . . 4 class ⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))
31	4, 7, 30	csb 3828	. . 3 class ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))
32	2, 3, 31	cmpt 5153	. 2 class (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))
33	1, 32	wceq 1539	1 wff VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))

This definition is referenced by:  vtxdgfval  27737