Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-vtxdg Structured version   Visualization version   GIF version

Definition df-vtxdg 40682
 Description: Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain 𝑢 "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 +𝑒 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.)
Assertion
Ref Expression
df-vtxdg VtxDeg = (𝑔 ∈ V ↦ (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
Distinct variable group:   𝑒,𝑔,𝑢,𝑣,𝑥

Detailed syntax breakdown of Definition df-vtxdg
StepHypRef Expression
1 cvtxdg 40681 . 2 class VtxDeg
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
4 vv . . . 4 setvar 𝑣
52cv 1474 . . . . 5 class 𝑔
6 cvtx 25673 . . . . 5 class Vtx
75, 6cfv 5804 . . . 4 class (Vtx‘𝑔)
8 ve . . . . 5 setvar 𝑒
9 ciedg 25674 . . . . . 6 class iEdg
105, 9cfv 5804 . . . . 5 class (iEdg‘𝑔)
11 vu . . . . . 6 setvar 𝑢
124cv 1474 . . . . . 6 class 𝑣
1311cv 1474 . . . . . . . . . 10 class 𝑢
14 vx . . . . . . . . . . . 12 setvar 𝑥
1514cv 1474 . . . . . . . . . . 11 class 𝑥
168cv 1474 . . . . . . . . . . 11 class 𝑒
1715, 16cfv 5804 . . . . . . . . . 10 class (𝑒𝑥)
1813, 17wcel 1977 . . . . . . . . 9 wff 𝑢 ∈ (𝑒𝑥)
1916cdm 5038 . . . . . . . . 9 class dom 𝑒
2018, 14, 19crab 2900 . . . . . . . 8 class {𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}
21 chash 12979 . . . . . . . 8 class #
2220, 21cfv 5804 . . . . . . 7 class (#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)})
2313csn 4125 . . . . . . . . . 10 class {𝑢}
2417, 23wceq 1475 . . . . . . . . 9 wff (𝑒𝑥) = {𝑢}
2524, 14, 19crab 2900 . . . . . . . 8 class {𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}
2625, 21cfv 5804 . . . . . . 7 class (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})
27 cxad 11820 . . . . . . 7 class +𝑒
2822, 26, 27co 6549 . . . . . 6 class ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))
2911, 12, 28cmpt 4643 . . . . 5 class (𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
308, 10, 29csb 3499 . . . 4 class (iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
314, 7, 30csb 3499 . . 3 class (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
322, 3, 31cmpt 4643 . 2 class (𝑔 ∈ V ↦ (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
331, 32wceq 1475 1 wff VtxDeg = (𝑔 ∈ V ↦ (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
 Colors of variables: wff setvar class This definition is referenced by:  vtxdgfval  40683
 Copyright terms: Public domain W3C validator