Metamath Proof Explorer

Theorem 0vtxrgr

Description: A null graph (with no vertices) is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Assertion 0vtxrgr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → ∀ k ∈ ℕ 0 * G RegGraph k

Proof

Step Hyp Ref Expression
1 simpr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ k ∈ ℕ 0 * → k ∈ ℕ 0 *
2 rzal ⊢ Vtx ⁡ G = ∅ → ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = k
3 2 ad2antlr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ k ∈ ℕ 0 * → ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = k
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
6 4 5 isrgr ⊢ G ∈ W ∧ k ∈ ℕ 0 * → G RegGraph k ↔ k ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = k
7 6 adantlr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ k ∈ ℕ 0 * → G RegGraph k ↔ k ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = k
8 1 3 7 mpbir2and ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ k ∈ ℕ 0 * → G RegGraph k
9 8 ralrimiva ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → ∀ k ∈ ℕ 0 * G RegGraph k