Theorem frusgrnn0

Description: In a nonempty finite k-regular simple graph, the degree of each vertex is finite. (Contributed by AV, 7-May-2021)

	Ref	Expression
Hypothesis	frusgrnn0.v	|- V = ( Vtx ` G )
Assertion	frusgrnn0	|- ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> K e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		frusgrnn0.v	|- V = ( Vtx ` G )
2		3simpb	|- ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> ( G e. FinUSGraph /\ V =/= (/) ) )
3		eqid	|- ( VtxDeg ` G ) = ( VtxDeg ` G )
4	1 3	rusgrprop0	|- ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) )
5	4	simp3d	|- ( G RegUSGraph K -> A. v e. V ( ( VtxDeg ` G ) ` v ) = K )
6	5	3ad2ant2	|- ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> A. v e. V ( ( VtxDeg ` G ) ` v ) = K )
7	1 3	fusgrregdegfi	|- ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> K e. NN0 ) )
8	2 6 7	sylc	|- ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> K e. NN0 )