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	⊢ 𝑅 = ( 𝑘 ∈ ℕ0* ↦ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 } )
Assertion	rgrx0nd	⊢ ( 𝑅 ‘ 0 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		rgrx0ndm.u	⊢ 𝑅 = ( 𝑘 ∈ ℕ0* ↦ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 } )
2	1	rgrx0ndm	⊢ 0 ∉ dom 𝑅
3	2	neli	⊢ ¬ 0 ∈ dom 𝑅
4		ndmfv	⊢ ( ¬ 0 ∈ dom 𝑅 → ( 𝑅 ‘ 0 ) = ∅ )
5	3 4	ax-mp	⊢ ( 𝑅 ‘ 0 ) = ∅