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 = ( Vtx ` G )
Assertion vtxdgfusgrf
|- ( G e. FinUSGraph -> ( VtxDeg ` G ) : V --> NN0 )

Proof

Step Hyp Ref Expression
1 vtxdgfusgrf.v
 |-  V = ( Vtx ` G )
2 fusgrfis
 |-  ( G e. FinUSGraph -> ( Edg ` G ) e. Fin )
3 fusgrusgr
 |-  ( G e. FinUSGraph -> G e. USGraph )
4 eqid
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 eqid
 |-  ( Edg ` G ) = ( Edg ` G )
6 4 5 usgredgffibi
 |-  ( G e. USGraph -> ( ( Edg ` G ) e. Fin <-> ( iEdg ` G ) e. Fin ) )
7 3 6 syl
 |-  ( G e. FinUSGraph -> ( ( Edg ` G ) e. Fin <-> ( iEdg ` G ) e. Fin ) )
8 usgrfun
 |-  ( G e. USGraph -> Fun ( iEdg ` G ) )
9 fundmfibi
 |-  ( Fun ( iEdg ` G ) -> ( ( iEdg ` G ) e. Fin <-> dom ( iEdg ` G ) e. Fin ) )
10 3 8 9 3syl
 |-  ( G e. FinUSGraph -> ( ( iEdg ` G ) e. Fin <-> dom ( iEdg ` G ) e. Fin ) )
11 7 10 bitrd
 |-  ( G e. FinUSGraph -> ( ( Edg ` G ) e. Fin <-> dom ( iEdg ` G ) e. Fin ) )
12 2 11 mpbid
 |-  ( G e. FinUSGraph -> dom ( iEdg ` G ) e. Fin )
13 eqid
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
14 1 4 13 vtxdgfisf
 |-  ( ( G e. FinUSGraph /\ dom ( iEdg ` G ) e. Fin ) -> ( VtxDeg ` G ) : V --> NN0 )
15 12 14 mpdan
 |-  ( G e. FinUSGraph -> ( VtxDeg ` G ) : V --> NN0 )