This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uhgriedg0edg0

Description: A hypergraph has no edges iff its edge function is empty. (Contributed by AV, 21-Oct-2020) (Proof shortened by AV, 8-Dec-2021)

Ref Expression
Assertion uhgriedg0edg0 ⊢ G ∈ UHGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅

Proof

Step Hyp Ref Expression
1 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
2 1 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ iEdg ⁡ G
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 1 3 edg0iedg0 ⊢ Fun ⁡ iEdg ⁡ G → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
5 2 4 syl ⊢ G ∈ UHGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅