Theorem 0grrgr

Description: The null graph represented by an empty set is k-regular for every k. (Contributed by AV, 26-Dec-2020)

	Ref	Expression
Assertion	0grrgr	$$⊢\forall k\in {\mathbb{N}}_0^{*}\varnothing \mathrm{RegGraph}k$$

Proof

Step	Hyp	Ref	Expression
1		0grrusgr	$$⊢\forall k\in {\mathbb{N}}_0^{*}\varnothing \mathrm{RegUSGraph}k$$
2		rusgrrgr	$$⊢\varnothing \mathrm{RegUSGraph}k\to \varnothing \mathrm{RegGraph}k$$
3	2	ralimi	$$⊢\forall k\in {\mathbb{N}}_0^{*}\varnothing \mathrm{RegUSGraph}k\to \forall k\in {\mathbb{N}}_0^{*}\varnothing \mathrm{RegGraph}k$$
4	1 3	ax-mp	$$⊢\forall k\in {\mathbb{N}}_0^{*}\varnothing \mathrm{RegGraph}k$$