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 27814
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 27813 . 2 class VtxDeg
2 vg . . 3 setvar 𝑔
3 cvv 3430 . . 3 class V
4 vv . . . 4 setvar 𝑣
52cv 1540 . . . . 5 class 𝑔
6 cvtx 27347 . . . . 5 class Vtx
75, 6cfv 6430 . . . 4 class (Vtx‘𝑔)
8 ve . . . . 5 setvar 𝑒
9 ciedg 27348 . . . . . 6 class iEdg
105, 9cfv 6430 . . . . 5 class (iEdg‘𝑔)
11 vu . . . . . 6 setvar 𝑢
124cv 1540 . . . . . 6 class 𝑣
1311cv 1540 . . . . . . . . . 10 class 𝑢
14 vx . . . . . . . . . . . 12 setvar 𝑥
1514cv 1540 . . . . . . . . . . 11 class 𝑥
168cv 1540 . . . . . . . . . . 11 class 𝑒
1715, 16cfv 6430 . . . . . . . . . 10 class (𝑒𝑥)
1813, 17wcel 2109 . . . . . . . . 9 wff 𝑢 ∈ (𝑒𝑥)
1916cdm 5588 . . . . . . . . 9 class dom 𝑒
2018, 14, 19crab 3069 . . . . . . . 8 class {𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}
21 chash 14025 . . . . . . . 8 class
2220, 21cfv 6430 . . . . . . 7 class (♯‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)})
2313csn 4566 . . . . . . . . . 10 class {𝑢}
2417, 23wceq 1541 . . . . . . . . 9 wff (𝑒𝑥) = {𝑢}
2524, 14, 19crab 3069 . . . . . . . 8 class {𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}
2625, 21cfv 6430 . . . . . . 7 class (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})
27 cxad 12828 . . . . . . 7 class +𝑒
2822, 26, 27co 7268 . . . . . 6 class ((♯‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))
2911, 12, 28cmpt 5161 . . . . 5 class (𝑢𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
308, 10, 29csb 3836 . . . 4 class (iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
314, 7, 30csb 3836 . . 3 class (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}})))
322, 3, 31cmpt 5161 . 2 class (𝑔 ∈ V ↦ (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
331, 32wceq 1541 1 wff VtxDeg = (𝑔 ∈ V ↦ (Vtx‘𝑔) / 𝑣(iEdg‘𝑔) / 𝑒(𝑢𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒𝑢 ∈ (𝑒𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒𝑥) = {𝑢}}))))
Colors of variables: wff setvar class
This definition is referenced by:  vtxdgfval  27815
  Copyright terms: Public domain W3C validator