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 Fin U V VtxDeg G U 0

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 Fin U V VtxDeg G U = x A | U I x + x A | I x = U
5 rabfi A Fin x A | U I x Fin
6 hashcl x A | U I x Fin x A | U I x 0
7 5 6 syl A Fin x A | U I x 0
8 rabfi A Fin x A | I x = U Fin
9 hashcl x A | I x = U Fin x A | I x = U 0
10 8 9 syl A Fin x A | I x = U 0
11 7 10 nn0addcld A Fin x A | U I x + x A | I x = U 0
12 11 adantr A Fin U V x A | U I x + x A | I x = U 0
13 4 12 eqeltrd A Fin U V VtxDeg G U 0