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 e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
2 1 uhgrfun 
 |-  ( G e. 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 e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )