Theorem 0grrgr

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

	Ref	Expression
Assertion	0grrgr	⊢ ∀ 𝑘 ∈ ℕ0* ∅ RegGraph 𝑘

Proof

Step	Hyp	Ref	Expression
1		0grrusgr	⊢ ∀ 𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘
2		rusgrrgr	⊢ ( ∅ RegUSGraph 𝑘 → ∅ RegGraph 𝑘 )
3	2	ralimi	⊢ ( ∀ 𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘 → ∀ 𝑘 ∈ ℕ0* ∅ RegGraph 𝑘 )
4	1 3	ax-mp	⊢ ∀ 𝑘 ∈ ℕ0* ∅ RegGraph 𝑘