Metamath Proof Explorer


Theorem vtxdgfusgr

Description: In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 12-Dec-2020)

Ref Expression
Hypothesis vtxdgfusgrf.v
|- V = ( Vtx ` G )
Assertion vtxdgfusgr
|- ( G e. FinUSGraph -> A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 )

Proof

Step Hyp Ref Expression
1 vtxdgfusgrf.v
 |-  V = ( Vtx ` G )
2 1 vtxdgfusgrf
 |-  ( G e. FinUSGraph -> ( VtxDeg ` G ) : V --> NN0 )
3 2 ffvelrnda
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> ( ( VtxDeg ` G ) ` v ) e. NN0 )
4 3 ralrimiva
 |-  ( G e. FinUSGraph -> A. v e. V ( ( VtxDeg ` G ) ` v ) e. NN0 )