Theorem 0grrusgr

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

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

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		vtxval0	$$⊢\mathrm{Vtx}\left(\varnothing \right)=\varnothing$$
3		iedgval0	$$⊢\mathrm{iEdg}\left(\varnothing \right)=\varnothing$$
4		0vtxrusgr	$$⊢\left(\varnothing \in \mathrm{V}\wedge \mathrm{Vtx}\left(\varnothing \right)=\varnothing \wedge \mathrm{iEdg}\left(\varnothing \right)=\varnothing \right)\to \forall k\in {\mathbb{N}}_0^{*}\varnothing \mathrm{RegUSGraph}k$$
5	1 2 3 4	mp3an	$$⊢\forall k\in {\mathbb{N}}_0^{*}\varnothing \mathrm{RegUSGraph}k$$