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 ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
2 1 uhgrfun ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
3 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4 1 3 edg0iedg0 ( Fun ( iEdg ‘ 𝐺 ) → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
5 2 4 syl ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )