Metamath Proof Explorer

Theorem uhgr0edg0rgrb

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

Ref Expression
Assertion uhgr0edg0rgrb ⊢G∈UHGraph→GRegGraph0↔Edg⁡G=∅

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢Edg⁡G=Edg⁡G
3 1 2 uhgrvd00 ⊢G∈UHGraph→∀v∈Vtx⁡GVtxDeg⁡G⁡v=0→Edg⁡G=∅
4 3 com12 ⊢∀v∈Vtx⁡GVtxDeg⁡G⁡v=0→G∈UHGraph→Edg⁡G=∅
5 4 adantl ⊢0∈ℕ0*∧∀v∈Vtx⁡GVtxDeg⁡G⁡v=0→G∈UHGraph→Edg⁡G=∅
6 eqid ⊢VtxDeg⁡G=VtxDeg⁡G
7 1 6 rgrprop ⊢GRegGraph0→0∈ℕ0*∧∀v∈Vtx⁡GVtxDeg⁡G⁡v=0
8 5 7 syl11 ⊢G∈UHGraph→GRegGraph0→Edg⁡G=∅
9 uhgr0edg0rgr ⊢G∈UHGraph∧Edg⁡G=∅→GRegGraph0
10 9 ex ⊢G∈UHGraph→Edg⁡G=∅→GRegGraph0
11 8 10 impbid ⊢G∈UHGraph→GRegGraph0↔Edg⁡G=∅