Metamath Proof Explorer


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