Definition df-vtxdg

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)

	Ref	Expression
Assertion	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 } } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvtxdg	|- VtxDeg
1		vg	|- g
2		cvv	|- _V
3		cvtx	|- Vtx
4	1	cv	|- g
5	4 3	cfv	|- ( Vtx ` g )
6		vv	|- v
7		ciedg	|- iEdg
8	4 7	cfv	|- ( iEdg ` g )
9		ve	|- e
10		vu	|- u
11	6	cv	|- v
12		chash	|- #
13		vx	|- x
14	9	cv	|- e
15	14	cdm	|- dom e
16	10	cv	|- u
17	13	cv	|- x
18	17 14	cfv	|- ( e ` x )
19	16 18	wcel	|- u e. ( e ` x )
20	19 13 15	crab	|- { x e. dom e | u e. ( e ` x ) }
21	20 12	cfv	|- ( # ` { x e. dom e | u e. ( e ` x ) } )
22		cxad	|- +e
23	16	csn	|- { u }
24	18 23	wceq	|- ( e ` x ) = { u }
25	24 13 15	crab	|- { x e. dom e | ( e ` x ) = { u } }
26	25 12	cfv	|- ( # ` { x e. dom e | ( e ` x ) = { u } } )
27	21 26 22	co	|- ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) )
28	10 11 27	cmpt	|- ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
29	9 8 28	csb	|- [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) )
30	6 5 29	csb	|- [_ ( 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 } } ) ) )
31	1 2 30	cmpt	|- ( 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 } } ) ) ) )
32	0 31	wceq	|- 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 } } ) ) ) )