Metamath Proof Explorer

Theorem 0edg0rgr

Description: A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Assertion 0edg0rgr ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ → G RegGraph 0

Proof

Step Hyp Ref Expression
1 simpr ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ ∧ v ∈ Vtx ⁡ G → v ∈ Vtx ⁡ G
2 simplr ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ ∧ v ∈ Vtx ⁡ G → iEdg ⁡ G = ∅
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 3 4 vtxdg0e ⊢ v ∈ Vtx ⁡ G ∧ iEdg ⁡ G = ∅ → VtxDeg ⁡ G ⁡ v = 0
6 1 2 5 syl2anc ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ ∧ v ∈ Vtx ⁡ G → VtxDeg ⁡ G ⁡ v = 0
7 6 ralrimiva ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ → ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = 0
8 0xnn0 ⊢ 0 ∈ ℕ 0 *
9 7 8 jctil ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ → 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = 0
10 8 a1i ⊢ iEdg ⁡ G = ∅ → 0 ∈ ℕ 0 *
11 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
12 3 11 isrgr ⊢ G ∈ W ∧ 0 ∈ ℕ 0 * → G RegGraph 0 ↔ 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = 0
13 10 12 sylan2 ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ → G RegGraph 0 ↔ 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = 0
14 9 13 mpbird ⊢ G ∈ W ∧ iEdg ⁡ G = ∅ → G RegGraph 0