Metamath Proof Explorer


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 V Vtx g / v iEdg g / e u v x dom e | u e x + 𝑒 x dom e | e x = u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvtxdg class VtxDeg
1 vg setvar g
2 cvv class V
3 cvtx class Vtx
4 1 cv setvar g
5 4 3 cfv class Vtx g
6 vv setvar v
7 ciedg class iEdg
8 4 7 cfv class iEdg g
9 ve setvar e
10 vu setvar u
11 6 cv setvar v
12 chash class .
13 vx setvar x
14 9 cv setvar e
15 14 cdm class dom e
16 10 cv setvar u
17 13 cv setvar x
18 17 14 cfv class e x
19 16 18 wcel wff u e x
20 19 13 15 crab class x dom e | u e x
21 20 12 cfv class x dom e | u e x
22 cxad class + 𝑒
23 16 csn class u
24 18 23 wceq wff e x = u
25 24 13 15 crab class x dom e | e x = u
26 25 12 cfv class x dom e | e x = u
27 21 26 22 co class x dom e | u e x + 𝑒 x dom e | e x = u
28 10 11 27 cmpt class u v x dom e | u e x + 𝑒 x dom e | e x = u
29 9 8 28 csb class iEdg g / e u v x dom e | u e x + 𝑒 x dom e | e x = u
30 6 5 29 csb class Vtx g / v iEdg g / e u v x dom e | u e x + 𝑒 x dom e | e x = u
31 1 2 30 cmpt class g V Vtx g / v iEdg g / e u v x dom e | u e x + 𝑒 x dom e | e x = u
32 0 31 wceq wff VtxDeg = g V Vtx g / v iEdg g / e u v x dom e | u e x + 𝑒 x dom e | e x = u