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 = ( k e. NN0* |-> { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k } )
Assertion	rgrx0nd	|- ( R ` 0 ) = (/)

Proof

Step	Hyp	Ref	Expression
1		rgrx0ndm.u	|- R = ( k e. NN0* |-> { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k } )
2	1	rgrx0ndm	|- 0 e/ dom R
3	2	neli	|- -. 0 e. dom R
4		ndmfv	|- ( -. 0 e. dom R -> ( R ` 0 ) = (/) )
5	3 4	ax-mp	|- ( R ` 0 ) = (/)