Metamath Proof Explorer

Theorem rusgrprop0

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

Ref Expression
Hypotheses isrusgr0.v 
|- V = ( Vtx ` G )
isrusgr0.d 
|- D = ( VtxDeg ` G )
Assertion rusgrprop0 
|- ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) )

Proof

Step Hyp Ref Expression
1 isrusgr0.v 
 |-  V = ( Vtx ` G )
2 isrusgr0.d 
 |-  D = ( VtxDeg ` G )
3 rusgrprop 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ G RegGraph K ) )
4 1 2 rgrprop 
 |-  ( G RegGraph K -> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) )
5 4 anim2i 
 |-  ( ( G e. USGraph /\ G RegGraph K ) -> ( G e. USGraph /\ ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
6 3anass 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) <-> ( G e. USGraph /\ ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
7 5 6 sylibr 
 |-  ( ( G e. USGraph /\ G RegGraph K ) -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) )
8 3 7 syl 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) )