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 classVtxDeg
1 vg setvarg
2 cvv classV
3 cvtx classVtx
4 1 cv setvarg
5 4 3 cfv classVtx⁡g
6 vv setvarv
7 ciedg classiEdg
8 4 7 cfv classiEdg⁡g
9 ve setvare
10 vu setvaru
11 6 cv setvarv
12 chash class.
13 vx setvarx
14 9 cv setvare
15 14 cdm classdom⁡e
16 10 cv setvaru
17 13 cv setvarx
18 17 14 cfv classe⁡x
19 16 18 wcel wffu∈e⁡x
20 19 13 15 crab classx∈dom⁡e|u∈e⁡x
21 20 12 cfv classx∈dom⁡e|u∈e⁡x
22 cxad class+𝑒
23 16 csn classu
24 18 23 wceq wffe⁡x=u
25 24 13 15 crab classx∈dom⁡e|e⁡x=u
26 25 12 cfv classx∈dom⁡e|e⁡x=u
27 21 26 22 co classx∈dom⁡e|u∈e⁡x+𝑒x∈dom⁡e|e⁡x=u
28 10 11 27 cmpt classu∈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 classg∈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 wffVtxDeg=g∈V⟼⦋Vtx⁡g/v⦌⦋iEdg⁡g/e⦌u∈v⟼x∈dom⁡e|u∈e⁡x+𝑒x∈dom⁡e|e⁡x=u