This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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