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 )