Definition df-vdgr 25021

Description: Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, we have to double-count those edges that contain u "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 +e 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 e. _V , e e. _V |-> ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )

Distinct variable group:   u, e, v, x

Detailed syntax breakdown of Definition df-vdgr

Step	Hyp	Ref	Expression
1		cvdg 25020	. 2 class VDeg
2		vv	. . 3 setvar v
3		ve	. . 3 setvar e
4		cvv 3109	. . 3 class _V
5		vu	. . . 4 setvar u
6	2	cv 1394	. . . 4 class v
7	5	cv 1394	. . . . . . . 8 class u
8		vx	. . . . . . . . . 10 setvar x
9	8	cv 1394	. . . . . . . . 9 class x
10	3	cv 1394	. . . . . . . . 9 class e
11	9, 10	cfv 5594	. . . . . . . 8 class ( e ` x )
12	7, 11	wcel 1819	. . . . . . 7 wff u e. ( e ` x )
13	10	cdm 5008	. . . . . . 7 class dom e
14	12, 8, 13	crab 2811	. . . . . 6 class { x e. dom e | u e. ( e ` x ) }
15		chash 12408	. . . . . 6 class #
16	14, 15	cfv 5594	. . . . 5 class ( # ` { x e. dom e | u e. ( e ` x ) } )
17	7	csn 4032	. . . . . . . 8 class { u }
18	11, 17	wceq 1395	. . . . . . 7 wff ( e ` x ) = { u }
19	18, 8, 13	crab 2811	. . . . . 6 class { x e. dom e | ( e ` x ) = { u } }
20	19, 15	cfv 5594	. . . . 5 class ( # ` { x e. dom e | ( e ` x ) = { u } } )
21		cxad 11341	. . . . 5 class +e
22	16, 20, 21	co 6296	. . . 4 class ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) )
23	5, 6, 22	cmpt 4515	. . 3 class ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
24	2, 3, 4, 4, 23	cmpt2 6298	. 2 class ( v e. _V , e e. _V |-> ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )
25	1, 24	wceq 1395	1 wff VDeg = ( v e. _V , e e. _V |-> ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )

This definition is referenced by:  vdgrfval  25022