Metamath Proof Explorer

Theorem isrgr

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

Ref Expression
Hypotheses isrgr.v 
|- V = ( Vtx ` G )
isrgr.d 
|- D = ( VtxDeg ` G )
Assertion isrgr 
|- ( ( G e. W /\ K e. Z ) -> ( 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 eleq1 
 |-  ( k = K -> ( k e. NN0* <-> K e. NN0* ) )
4 3 adantl 
 |-  ( ( g = G /\ k = K ) -> ( k e. NN0* <-> K e. NN0* ) )
5 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
6 5 adantr 
 |-  ( ( g = G /\ k = K ) -> ( Vtx ` g ) = ( Vtx ` G ) )
7 fveq2 
 |-  ( g = G -> ( VtxDeg ` g ) = ( VtxDeg ` G ) )
8 7 fveq1d 
 |-  ( g = G -> ( ( VtxDeg ` g ) ` v ) = ( ( VtxDeg ` G ) ` v ) )
9 8 adantr 
 |-  ( ( g = G /\ k = K ) -> ( ( VtxDeg ` g ) ` v ) = ( ( VtxDeg ` G ) ` v ) )
10 simpr 
 |-  ( ( g = G /\ k = K ) -> k = K )
11 9 10 eqeq12d 
 |-  ( ( g = G /\ k = K ) -> ( ( ( VtxDeg ` g ) ` v ) = k <-> ( ( VtxDeg ` G ) ` v ) = K ) )
12 6 11 raleqbidv 
 |-  ( ( g = G /\ k = K ) -> ( A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k <-> A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = K ) )
13 4 12 anbi12d 
 |-  ( ( g = G /\ k = K ) -> ( ( k e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k ) <-> ( K e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = K ) ) )
14 df-rgr 
 |-  RegGraph = { <. g , k >. | ( k e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k ) }
15 13 14 brabga 
 |-  ( ( G e. W /\ K e. Z ) -> ( G RegGraph K <-> ( K e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = K ) ) )
16 2 fveq1i 
 |-  ( D ` v ) = ( ( VtxDeg ` G ) ` v )
17 16 eqeq1i 
 |-  ( ( D ` v ) = K <-> ( ( VtxDeg ` G ) ` v ) = K )
18 1 17 raleqbii 
 |-  ( A. v e. V ( D ` v ) = K <-> A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = K )
19 18 bicomi 
 |-  ( A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = K <-> A. v e. V ( D ` v ) = K )
20 19 a1i 
 |-  ( ( G e. W /\ K e. Z ) -> ( A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = K <-> A. v e. V ( D ` v ) = K ) )
21 20 anbi2d 
 |-  ( ( G e. W /\ K e. Z ) -> ( ( K e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = K ) <-> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )
22 15 21 bitrd 
 |-  ( ( G e. W /\ K e. Z ) -> ( G RegGraph K <-> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) )