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

Proof

Step Hyp Ref Expression
1 uhgriedg0edg0 
 |-  ( G e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
2 1 biimpa 
 |-  ( ( G e. UHGraph /\ ( Edg ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
3 0edg0rgr 
 |-  ( ( G e. UHGraph /\ ( iEdg ` G ) = (/) ) -> G RegGraph 0 )
4 2 3 syldan 
 |-  ( ( G e. UHGraph /\ ( Edg ` G ) = (/) ) -> G RegGraph 0 )