Definition df-vtxdg 16733

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 infinite), the extended addition +e is used for the summation of the number of "ordinary" edges" and the number of "loops".

Because we cannot in general show that an arbitrary set is either finite or infinite (see inffiexmid 7217), this definition is not as general as it may appear. But we keep it for consistency with the Metamath Proof Explorer. (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 16732	. 2 class VtxDeg
2		vg	. . 3 setvar g
3		cvv 2821	. . 3 class _V
4		vv	. . . 4 setvar v
5	2	cv 1401	. . . . 5 class g
6		cvtx 16458	. . . . 5 class Vtx
7	5, 6	cfv 5380	. . . 4 class (Vtx ` g )
8		ve	. . . . 5 setvar e
9		ciedg 16459	. . . . . 6 class iEdg
10	5, 9	cfv 5380	. . . . 5 class (iEdg ` g )
11		vu	. . . . . 6 setvar u
12	4	cv 1401	. . . . . 6 class v
13	11	cv 1401	. . . . . . . . . 10 class u
14		vx	. . . . . . . . . . . 12 setvar x
15	14	cv 1401	. . . . . . . . . . 11 class x
16	8	cv 1401	. . . . . . . . . . 11 class e
17	15, 16	cfv 5380	. . . . . . . . . 10 class ( e ` x )
18	13, 17	wcel 2209	. . . . . . . . 9 wff u e. ( e ` x )
19	16	cdm 4776	. . . . . . . . 9 class dom e
20	18, 14, 19	crab 2532	. . . . . . . 8 class { x e. dom e | u e. ( e ` x ) }
21		chash 11236	. . . . . . . 8 class ♯
22	20, 21	cfv 5380	. . . . . . 7 class (♯ ` { x e. dom e | u e. ( e ` x ) } )
23	13	csn 3709	. . . . . . . . . 10 class { u }
24	17, 23	wceq 1402	. . . . . . . . 9 wff ( e ` x ) = { u }
25	24, 14, 19	crab 2532	. . . . . . . 8 class { x e. dom e | ( e ` x ) = { u } }
26	25, 21	cfv 5380	. . . . . . 7 class (♯ ` { x e. dom e | ( e ` x ) = { u } } )
27		cxad 10189	. . . . . . 7 class +e
28	22, 26, 27	co 6088	. . . . . 6 class ( (♯ ` { x e. dom e | u e. ( e ` x ) } ) +e (♯ ` { x e. dom e | ( e ` x ) = { u } } ) )
29	11, 12, 28	cmpt 4193	. . . . 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 3147	. . . 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 3147	. . 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 4193	. 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 1402	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 used by:  vtxdgfval  16734