Definition df-vdgr 26421

Description: Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, 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.)

Assertion

Ref	Expression
df-vdgr	⊢ VDeg = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))

Distinct variable group:   𝑢,𝑒,𝑣,𝑥

Detailed syntax breakdown of Definition df-vdgr

Step	Hyp	Ref	Expression
1		cvdg 26420	. 2 class VDeg
2		vv	. . 3 setvar 𝑣
3		ve	. . 3 setvar 𝑒
4		cvv 3173	. . 3 class V
5		vu	. . . 4 setvar 𝑢
6	2	cv 1474	. . . 4 class 𝑣
7	5	cv 1474	. . . . . . . 8 class 𝑢
8		vx	. . . . . . . . . 10 setvar 𝑥
9	8	cv 1474	. . . . . . . . 9 class 𝑥
10	3	cv 1474	. . . . . . . . 9 class 𝑒
11	9, 10	cfv 5804	. . . . . . . 8 class (𝑒‘𝑥)
12	7, 11	wcel 1977	. . . . . . 7 wff 𝑢 ∈ (𝑒‘𝑥)
13	10	cdm 5038	. . . . . . 7 class dom 𝑒
14	12, 8, 13	crab 2900	. . . . . 6 class {𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}
15		chash 12979	. . . . . 6 class #
16	14, 15	cfv 5804	. . . . 5 class (#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)})
17	7	csn 4125	. . . . . . . 8 class {𝑢}
18	11, 17	wceq 1475	. . . . . . 7 wff (𝑒‘𝑥) = {𝑢}
19	18, 8, 13	crab 2900	. . . . . 6 class {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}
20	19, 15	cfv 5804	. . . . 5 class (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})
21		cxad 11820	. . . . 5 class +𝑒
22	16, 20, 21	co 6549	. . . 4 class ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))
23	5, 6, 22	cmpt 4643	. . 3 class (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))
24	2, 3, 4, 4, 23	cmpt2 6551	. 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))
25	1, 24	wceq 1475	1 wff VDeg = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))

This definition is referenced by:  vdgrfval  26422