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	⊢ ∀ 𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		vtxval0	⊢ ( Vtx ‘ ∅ ) = ∅
3		iedgval0	⊢ ( iEdg ‘ ∅ ) = ∅
4		0vtxrusgr	⊢ ( ( ∅ ∈ V ∧ ( Vtx ‘ ∅ ) = ∅ ∧ ( iEdg ‘ ∅ ) = ∅ ) → ∀ 𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘 )
5	1 2 3 4	mp3an	⊢ ∀ 𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘