Metamath Proof Explorer

Theorem vtxdgfisnn0

Description: The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 11-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypotheses vtxdgf.v 
|- V = ( Vtx ` G )
vtxdg0e.i 
|- I = ( iEdg ` G )
vtxdgfisnn0.a 
|- A = dom I
Assertion vtxdgfisnn0 
|- ( ( A e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) e. NN0 )

Proof

Step Hyp Ref Expression
1 vtxdgf.v 
 |-  V = ( Vtx ` G )
2 vtxdg0e.i 
 |-  I = ( iEdg ` G )
3 vtxdgfisnn0.a 
 |-  A = dom I
4 1 2 3 vtxdgfival 
 |-  ( ( A e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
5 rabfi 
 |-  ( A e. Fin -> { x e. A | U e. ( I ` x ) } e. Fin )
6 hashcl 
 |-  ( { x e. A | U e. ( I ` x ) } e. Fin -> ( # ` { x e. A | U e. ( I ` x ) } ) e. NN0 )
7 5 6 syl 
 |-  ( A e. Fin -> ( # ` { x e. A | U e. ( I ` x ) } ) e. NN0 )
8 rabfi 
 |-  ( A e. Fin -> { x e. A | ( I ` x ) = { U } } e. Fin )
9 hashcl 
 |-  ( { x e. A | ( I ` x ) = { U } } e. Fin -> ( # ` { x e. A | ( I ` x ) = { U } } ) e. NN0 )
10 8 9 syl 
 |-  ( A e. Fin -> ( # ` { x e. A | ( I ` x ) = { U } } ) e. NN0 )
11 7 10 nn0addcld 
 |-  ( A e. Fin -> ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) e. NN0 )
12 11 adantr 
 |-  ( ( A e. Fin /\ U e. V ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) e. NN0 )
13 4 12 eqeltrd 
 |-  ( ( A e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) e. NN0 )