Definition df-vtxdg 16137

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 7097), 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 16136	. 2 class VtxDeg
2		vg	. . 3 setvar g
3		cvv 2802	. . 3 class _V
4		vv	. . . 4 setvar v
5	2	cv 1396	. . . . 5 class g
6		cvtx 15862	. . . . 5 class Vtx
7	5, 6	cfv 5326	. . . 4 class (Vtx ` g )
8		ve	. . . . 5 setvar e
9		ciedg 15863	. . . . . 6 class iEdg
10	5, 9	cfv 5326	. . . . 5 class (iEdg ` g )
11		vu	. . . . . 6 setvar u
12	4	cv 1396	. . . . . 6 class v
13	11	cv 1396	. . . . . . . . . 10 class u
14		vx	. . . . . . . . . . . 12 setvar x
15	14	cv 1396	. . . . . . . . . . 11 class x
16	8	cv 1396	. . . . . . . . . . 11 class e
17	15, 16	cfv 5326	. . . . . . . . . 10 class ( e ` x )
18	13, 17	wcel 2202	. . . . . . . . 9 wff u e. ( e ` x )
19	16	cdm 4725	. . . . . . . . 9 class dom e
20	18, 14, 19	crab 2514	. . . . . . . 8 class { x e. dom e | u e. ( e ` x ) }
21		chash 11036	. . . . . . . 8 class ♯
22	20, 21	cfv 5326	. . . . . . 7 class (♯ ` { x e. dom e | u e. ( e ` x ) } )
23	13	csn 3669	. . . . . . . . . 10 class { u }
24	17, 23	wceq 1397	. . . . . . . . 9 wff ( e ` x ) = { u }
25	24, 14, 19	crab 2514	. . . . . . . 8 class { x e. dom e | ( e ` x ) = { u } }
26	25, 21	cfv 5326	. . . . . . 7 class (♯ ` { x e. dom e | ( e ` x ) = { u } } )
27		cxad 10004	. . . . . . 7 class +e
28	22, 26, 27	co 6017	. . . . . 6 class ( (♯ ` { x e. dom e | u e. ( e ` x ) } ) +e (♯ ` { x e. dom e | ( e ` x ) = { u } } ) )
29	11, 12, 28	cmpt 4150	. . . . 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 3127	. . . 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 3127	. . 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 4150	. 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 1397	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  16138