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