Metamath Proof Explorer


Theorem 0vtxrgr

Description: A null graph (with no vertices) is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Assertion 0vtxrgr
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> A. k e. NN0* G RegGraph k )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ k e. NN0* ) -> k e. NN0* )
2 rzal
 |-  ( ( Vtx ` G ) = (/) -> A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = k )
3 2 ad2antlr
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ k e. NN0* ) -> A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = k )
4 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 eqid
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
6 4 5 isrgr
 |-  ( ( G e. W /\ k e. NN0* ) -> ( G RegGraph k <-> ( k e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = k ) ) )
7 6 adantlr
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ k e. NN0* ) -> ( G RegGraph k <-> ( k e. NN0* /\ A. v e. ( Vtx ` G ) ( ( VtxDeg ` G ) ` v ) = k ) ) )
8 1 3 7 mpbir2and
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ k e. NN0* ) -> G RegGraph k )
9 8 ralrimiva
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> A. k e. NN0* G RegGraph k )