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	ffvelcdmda	|- ( ( 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 )