Metamath Proof Explorer

Theorem usgr0edg0rusgr

Description: A simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018) (Revised by AV, 19-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

Ref Expression
Assertion usgr0edg0rusgr ⊢ G ∈ USGraph → G RegUSGraph 0 ↔ Edg ⁡ G = ∅

Proof

Step Hyp Ref Expression
1 0nn0 ⊢ 0 ∈ ℕ 0
2 isrusgr ⊢ G ∈ USGraph ∧ 0 ∈ ℕ 0 → G RegUSGraph 0 ↔ G ∈ USGraph ∧ G RegGraph 0
3 1 2 mpan2 ⊢ G ∈ USGraph → G RegUSGraph 0 ↔ G ∈ USGraph ∧ G RegGraph 0
4 ibar ⊢ G ∈ USGraph → G RegGraph 0 ↔ G ∈ USGraph ∧ G RegGraph 0
5 usgruhgr ⊢ G ∈ USGraph → G ∈ UHGraph
6 uhgr0edg0rgrb ⊢ G ∈ UHGraph → G RegGraph 0 ↔ Edg ⁡ G = ∅
7 5 6 syl ⊢ G ∈ USGraph → G RegGraph 0 ↔ Edg ⁡ G = ∅
8 3 4 7 3bitr2d ⊢ G ∈ USGraph → G RegUSGraph 0 ↔ Edg ⁡ G = ∅