Theorem rgrprop

Description: The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018) (Revised by AV, 26-Dec-2020)

	Ref	Expression
Hypotheses	isrgr.v	|- V = ( Vtx ` G )
	isrgr.d	|- D = ( VtxDeg ` G )
Assertion	rgrprop	|- ( G RegGraph K -> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) )

Proof

Step	Hyp	Ref	Expression
1		isrgr.v	|- V = ( Vtx ` G )
2		isrgr.d	|- D = ( VtxDeg ` G )
3		df-rgr	|- RegGraph = { <. g , k >. | ( k e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k ) }
4	3	bropaex12	|- ( G RegGraph K -> ( G e. _V /\ K e. _V ) )
5	1 2	isrgr	|- ( ( G e. _V /\ K e. _V ) -> ( G RegGraph K <-> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
6	5	biimpd	|- ( ( G e. _V /\ K e. _V ) -> ( G RegGraph K -> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
7	4 6	mpcom	|- ( G RegGraph K -> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) )