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 )