Metamath Proof Explorer

Theorem 0vtxrusgr

Description: A graph with no vertices and an empty edge function is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Assertion 0vtxrusgr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → ∀ k ∈ ℕ 0 * G RegUSGraph k

Proof

Step Hyp Ref Expression
1 usgr0v ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ USGraph
2 1 adantr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ ∧ k ∈ ℕ 0 * → G ∈ USGraph
3 0vtxrgr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → ∀ v ∈ ℕ 0 * G RegGraph v
4 breq2 ⊢ v = k → G RegGraph v ↔ G RegGraph k
5 4 rspccv ⊢ ∀ v ∈ ℕ 0 * G RegGraph v → k ∈ ℕ 0 * → G RegGraph k
6 3 5 syl ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → k ∈ ℕ 0 * → G RegGraph k
7 6 3adant3 ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → k ∈ ℕ 0 * → G RegGraph k
8 7 imp ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ ∧ k ∈ ℕ 0 * → G RegGraph k
9 isrusgr ⊢ G ∈ W ∧ k ∈ ℕ 0 * → G RegUSGraph k ↔ G ∈ USGraph ∧ G RegGraph k
10 9 3ad2antl1 ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ ∧ k ∈ ℕ 0 * → G RegUSGraph k ↔ G ∈ USGraph ∧ G RegGraph k
11 2 8 10 mpbir2and ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ ∧ k ∈ ℕ 0 * → G RegUSGraph k
12 11 ralrimiva ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → ∀ k ∈ ℕ 0 * G RegUSGraph k