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 → G RegGraph 0 ↔ 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 ⁡ G VtxDeg ⁡ G ⁡ v = 0 → Edg ⁡ G = ∅
4 3 com12 ⊢ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = 0 → G ∈ UHGraph → Edg ⁡ G = ∅
5 4 adantl ⊢ 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = 0 → G ∈ UHGraph → Edg ⁡ G = ∅
6 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
7 1 6 rgrprop ⊢ G RegGraph 0 → 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ G VtxDeg ⁡ G ⁡ v = 0
8 5 7 syl11 ⊢ G ∈ UHGraph → G RegGraph 0 → Edg ⁡ G = ∅
9 uhgr0edg0rgr ⊢ G ∈ UHGraph ∧ Edg ⁡ G = ∅ → G RegGraph 0
10 9 ex ⊢ G ∈ UHGraph → Edg ⁡ G = ∅ → G RegGraph 0
11 8 10 impbid ⊢ G ∈ UHGraph → G RegGraph 0 ↔ Edg ⁡ G = ∅