Metamath Proof Explorer

Theorem uhgr0edg0rgr

Description: A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020)

Ref Expression
Assertion uhgr0edg0rgr ⊢ G ∈ UHGraph ∧ Edg ⁡ G = ∅ → G RegGraph 0

Proof

Step Hyp Ref Expression
1 uhgriedg0edg0 ⊢ G ∈ UHGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
2 1 biimpa ⊢ G ∈ UHGraph ∧ Edg ⁡ G = ∅ → iEdg ⁡ G = ∅
3 0edg0rgr ⊢ G ∈ UHGraph ∧ iEdg ⁡ G = ∅ → G RegGraph 0
4 2 3 syldan ⊢ G ∈ UHGraph ∧ Edg ⁡ G = ∅ → G RegGraph 0