Metamath Proof Explorer


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 𝑘