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

Metamath Proof Explorer

Theorem vtxdgf

Description: The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 10-Dec-2020)

Ref Expression
Hypothesis vtxdgf.v 
|- V = ( Vtx ` G )
Assertion vtxdgf 
|- ( G e. W -> ( VtxDeg ` G ) : V --> NN0* )

Proof

Step Hyp Ref Expression
1 vtxdgf.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
4 1 2 3 vtxdgfval 
 |-  ( G e. W -> ( VtxDeg ` G ) = ( u e. V |-> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) ) )
5 eqid 
 |-  { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } = { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) }
6 fvex 
 |-  ( iEdg ` G ) e. _V
7 dmexg 
 |-  ( ( iEdg ` G ) e. _V -> dom ( iEdg ` G ) e. _V )
8 6 7 mp1i 
 |-  ( ( G e. W /\ u e. V ) -> dom ( iEdg ` G ) e. _V )
9 5 8 rabexd 
 |-  ( ( G e. W /\ u e. V ) -> { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } e. _V )
10 hashxnn0 
 |-  ( { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } e. _V -> ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) e. NN0* )
11 9 10 syl 
 |-  ( ( G e. W /\ u e. V ) -> ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) e. NN0* )
12 eqid 
 |-  { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } }
13 12 8 rabexd 
 |-  ( ( G e. W /\ u e. V ) -> { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } e. _V )
14 hashxnn0 
 |-  ( { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } e. _V -> ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) e. NN0* )
15 13 14 syl 
 |-  ( ( G e. W /\ u e. V ) -> ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) e. NN0* )
16 xnn0xaddcl 
 |-  ( ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) e. NN0* /\ ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) e. NN0* ) -> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) e. NN0* )
17 11 15 16 syl2anc 
 |-  ( ( G e. W /\ u e. V ) -> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) e. NN0* )
18 4 17 fmpt3d 
 |-  ( G e. W -> ( VtxDeg ` G ) : V --> NN0* )