MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vtxdg Structured version   Visualization version   GIF version

Definition df-vtxdg 26256
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 26255 . 2 class VtxDeg
2 vg . . 3 setvar 𝑔
3 cvv 3186 . . 3 class V
4 vv . . . 4 setvar 𝑣
52cv 1479 . . . . 5 class 𝑔
6 cvtx 25781 . . . . 5 class Vtx
75, 6cfv 5849 . . . 4 class (Vtx‘𝑔)
8 ve . . . . 5 setvar 𝑒
9 ciedg 25782 . . . . . 6 class iEdg
105, 9cfv 5849 . . . . 5 class (iEdg‘𝑔)
11 vu . . . . . 6 setvar 𝑢
124cv 1479 . . . . . 6 class 𝑣
1311cv 1479 . . . . . . . . . 10 class 𝑢
14 vx . . . . . . . . . . . 12 setvar 𝑥
1514cv 1479 . . . . . . . . . . 11 class 𝑥
168cv 1479 . . . . . . . . . . 11 class 𝑒
1715, 16cfv 5849 . . . . . . . . . 10 class (𝑒𝑥)
1813, 17wcel 1987 . . . . . . . . 9 wff 𝑢 ∈ (𝑒𝑥)
1916cdm 5076 . . . . . . . . 9 class dom 𝑒
2018, 14, 19crab 2911 . . . . . . . 8 class {𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}
21 chash 13060 . . . . . . . 8 class #
2220, 21cfv 5849 . . . . . . 7 class (#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)})
2313csn 4150 . . . . . . . . . 10 class {𝑢}
2417, 23wceq 1480 . . . . . . . . 9 wff (𝑒𝑥) = {𝑢}
2524, 14, 19crab 2911 . . . . . . . 8 class {𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}
2625, 21cfv 5849 . . . . . . 7 class (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})
27 cxad 11891 . . . . . . 7 class +𝑒
2822, 26, 27co 6607 . . . . . 6 class ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))
2911, 12, 28cmpt 4675 . . . . 5 class (𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
308, 10, 29csb 3515 . . . 4 class (iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
314, 7, 30csb 3515 . . 3 class (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
322, 3, 31cmpt 4675 . 2 class (𝑔 ∈ V ↦ (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
331, 32wceq 1480 1 wff VtxDeg = (𝑔 ∈ V ↦ (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
Colors of variables: wff setvar class
This definition is referenced by:  vtxdgfval  26257
  Copyright terms: Public domain W3C validator