Definition df-vtxdg 26362

Description: Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, 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.) (Revised by AV, 9-Dec-2020.)

Assertion

Ref	Expression
df-vtxdg	|- VtxDeg = ( g e. _V |-> [_ (Vtx ` g ) / v ]_ [_ (iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )

Distinct variable group:   e, g, u, v, x

Detailed syntax breakdown of Definition df-vtxdg

Step	Hyp	Ref	Expression
1		cvtxdg 26361	. 2 class VtxDeg
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vv	. . . 4 setvar v
5	2	cv 1482	. . . . 5 class g
6		cvtx 25874	. . . . 5 class Vtx
7	5, 6	cfv 5888	. . . 4 class (Vtx ` g )
8		ve	. . . . 5 setvar e
9		ciedg 25875	. . . . . 6 class iEdg
10	5, 9	cfv 5888	. . . . 5 class (iEdg ` g )
11		vu	. . . . . 6 setvar u
12	4	cv 1482	. . . . . 6 class v
13	11	cv 1482	. . . . . . . . . 10 class u
14		vx	. . . . . . . . . . . 12 setvar x
15	14	cv 1482	. . . . . . . . . . 11 class x
16	8	cv 1482	. . . . . . . . . . 11 class e
17	15, 16	cfv 5888	. . . . . . . . . 10 class ( e ` x )
18	13, 17	wcel 1990	. . . . . . . . 9 wff u e. ( e ` x )
19	16	cdm 5114	. . . . . . . . 9 class dom e
20	18, 14, 19	crab 2916	. . . . . . . 8 class { x e. dom e | u e. ( e ` x ) }
21		chash 13117	. . . . . . . 8 class #
22	20, 21	cfv 5888	. . . . . . 7 class ( # ` { x e. dom e | u e. ( e ` x ) } )
23	13	csn 4177	. . . . . . . . . 10 class { u }
24	17, 23	wceq 1483	. . . . . . . . 9 wff ( e ` x ) = { u }
25	24, 14, 19	crab 2916	. . . . . . . 8 class { x e. dom e | ( e ` x ) = { u } }
26	25, 21	cfv 5888	. . . . . . 7 class ( # ` { x e. dom e | ( e ` x ) = { u } } )
27		cxad 11944	. . . . . . 7 class +e
28	22, 26, 27	co 6650	. . . . . 6 class ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) )
29	11, 12, 28	cmpt 4729	. . . . 5 class ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
30	8, 10, 29	csb 3533	. . . 4 class [_ (iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
31	4, 7, 30	csb 3533	. . 3 class [_ (Vtx ` g ) / v ]_ [_ (iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
32	2, 3, 31	cmpt 4729	. 2 class ( g e. _V |-> [_ (Vtx ` g ) / v ]_ [_ (iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )
33	1, 32	wceq 1483	1 wff VtxDeg = ( g e. _V |-> [_ (Vtx ` g ) / v ]_ [_ (iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )

This definition is referenced by:  vtxdgfval  26363