Theorem rgrx0nd

Description: The potentially alternatively defined k-regular graphs is not defined for k=0. (Contributed by AV, 28-Dec-2020)

	Ref	Expression
Hypothesis	rgrx0ndm.u	$$⊢R=\left(k\in {\mathbb{N}}_0^{*}⟼\left\{g|\forall v\in \mathrm{Vtx}\left(g\right)\mathrm{VtxDeg}\left(g\right)\left(v\right)=k\right\}\right)$$
Assertion	rgrx0nd	$$⊢R\left(0\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rgrx0ndm.u	$$⊢R=\left(k\in {\mathbb{N}}_0^{*}⟼\left\{g|\forall v\in \mathrm{Vtx}\left(g\right)\mathrm{VtxDeg}\left(g\right)\left(v\right)=k\right\}\right)$$
2	1	rgrx0ndm	$$⊢0\notin \mathrm{dom}R$$
3	2	neli	$$⊢\neg 0\in \mathrm{dom}R$$
4		ndmfv	$$⊢\neg 0\in \mathrm{dom}R\to R\left(0\right)=\varnothing$$
5	3 4	ax-mp	$$⊢R\left(0\right)=\varnothing$$