Metamath Proof Explorer


Theorem vtxdgfusgrf

Description: The vertex degree function on finite simple graphs is a function from vertices to nonnegative integers. (Contributed by AV, 12-Dec-2020)

Ref Expression
Hypothesis vtxdgfusgrf.v V=VtxG
Assertion vtxdgfusgrf GFinUSGraphVtxDegG:V0

Proof

Step Hyp Ref Expression
1 vtxdgfusgrf.v V=VtxG
2 fusgrfis GFinUSGraphEdgGFin
3 fusgrusgr GFinUSGraphGUSGraph
4 eqid iEdgG=iEdgG
5 eqid EdgG=EdgG
6 4 5 usgredgffibi GUSGraphEdgGFiniEdgGFin
7 3 6 syl GFinUSGraphEdgGFiniEdgGFin
8 usgrfun GUSGraphFuniEdgG
9 fundmfibi FuniEdgGiEdgGFindomiEdgGFin
10 3 8 9 3syl GFinUSGraphiEdgGFindomiEdgGFin
11 7 10 bitrd GFinUSGraphEdgGFindomiEdgGFin
12 2 11 mpbid GFinUSGraphdomiEdgGFin
13 eqid domiEdgG=domiEdgG
14 1 4 13 vtxdgfisf GFinUSGraphdomiEdgGFinVtxDegG:V0
15 12 14 mpdan GFinUSGraphVtxDegG:V0