Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-vdgr Unicode version

Definition df-vdgr 23880
Description: Define the vertex degree function for an undirected multigraph. 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. (Contributed by Mario Carneiro, 12-Mar-2015.)
Assertion
Ref Expression
df-vdgr  |- VDeg  =  ( v  e.  _V , 
e  e.  _V  |->  ( u  e.  v  |->  ( ( # `  {
x  e.  dom  e  |  u  e.  (
e `  x ) } )  +  (
# `  { x  e.  dom  e  |  ( e `  x )  =  { u } } ) ) ) )
Distinct variable group:    u, e, v, x

Detailed syntax breakdown of Definition df-vdgr
StepHypRef Expression
1 cvdg 23877 . 2  class VDeg
2 vv . . 3  set  v
3 ve . . 3  set  e
4 cvv 2801 . . 3  class  _V
5 vu . . . 4  set  u
62cv 1631 . . . 4  class  v
75cv 1631 . . . . . . . 8  class  u
8 vx . . . . . . . . . 10  set  x
98cv 1631 . . . . . . . . 9  class  x
103cv 1631 . . . . . . . . 9  class  e
119, 10cfv 5271 . . . . . . . 8  class  ( e `
 x )
127, 11wcel 1696 . . . . . . 7  wff  u  e.  ( e `  x
)
1310cdm 4705 . . . . . . 7  class  dom  e
1412, 8, 13crab 2560 . . . . . 6  class  { x  e.  dom  e  |  u  e.  ( e `  x ) }
15 chash 11353 . . . . . 6  class  #
1614, 15cfv 5271 . . . . 5  class  ( # `  { x  e.  dom  e  |  u  e.  ( e `  x
) } )
177csn 3653 . . . . . . . 8  class  { u }
1811, 17wceq 1632 . . . . . . 7  wff  ( e `
 x )  =  { u }
1918, 8, 13crab 2560 . . . . . 6  class  { x  e.  dom  e  |  ( e `  x )  =  { u } }
2019, 15cfv 5271 . . . . 5  class  ( # `  { x  e.  dom  e  |  ( e `  x )  =  {
u } } )
21 caddc 8756 . . . . 5  class  +
2216, 20, 21co 5874 . . . 4  class  ( (
# `  { x  e.  dom  e  |  u  e.  ( e `  x ) } )  +  ( # `  {
x  e.  dom  e  |  ( e `  x )  =  {
u } } ) )
235, 6, 22cmpt 4093 . . 3  class  ( u  e.  v  |->  ( (
# `  { x  e.  dom  e  |  u  e.  ( e `  x ) } )  +  ( # `  {
x  e.  dom  e  |  ( e `  x )  =  {
u } } ) ) )
242, 3, 4, 4, 23cmpt2 5876 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  ( u  e.  v  |->  ( (
# `  { x  e.  dom  e  |  u  e.  ( e `  x ) } )  +  ( # `  {
x  e.  dom  e  |  ( e `  x )  =  {
u } } ) ) ) )
251, 24wceq 1632 1  wff VDeg  =  ( v  e.  _V , 
e  e.  _V  |->  ( u  e.  v  |->  ( ( # `  {
x  e.  dom  e  |  u  e.  (
e `  x ) } )  +  (
# `  { x  e.  dom  e  |  ( e `  x )  =  { u } } ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  vdgrfval  23904
  Copyright terms: Public domain W3C validator