Metamath Proof Explorer

Theorem isrusgr0

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

Ref Expression
Hypotheses isrusgr0.v 
|- V = ( Vtx ` G )
isrusgr0.d 
|- D = ( VtxDeg ` G )
Assertion isrusgr0 
|- ( ( G e. W /\ K e. Z ) -> ( 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 isrusgr 
 |-  ( ( G e. W /\ K e. Z ) -> ( G RegUSGraph K <-> ( G e. USGraph /\ G RegGraph K ) ) )
4 1 2 isrgr 
 |-  ( ( G e. W /\ K e. Z ) -> ( G RegGraph K <-> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
5 4 anbi2d 
 |-  ( ( G e. W /\ K e. Z ) -> ( ( 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 bitr4di 
 |-  ( ( G e. W /\ K e. Z ) -> ( ( G e. USGraph /\ G RegGraph K ) <-> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
8 3 7 bitrd 
 |-  ( ( G e. W /\ K e. Z ) -> ( G RegUSGraph K <-> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )