Metamath Proof Explorer

Theorem upgracycumgr

Description: An acyclic pseudograph is a multigraph. (Contributed by BTernaryTau, 15-Oct-2023)

Ref Expression
Assertion upgracycumgr 
|- ( ( G e. UPGraph /\ G e. AcyclicGraph ) -> G e. UMGraph )

Proof

Step Hyp Ref Expression
1 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
2 1 anim1ci 
 |-  ( ( G e. UPGraph /\ G e. AcyclicGraph ) -> ( G e. AcyclicGraph /\ G e. UHGraph ) )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 3 4 acycgrislfgr 
 |-  ( ( G e. AcyclicGraph /\ G e. UHGraph ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } )
6 2 5 syl 
 |-  ( ( G e. UPGraph /\ G e. AcyclicGraph ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } )
7 3 4 umgrislfupgr 
 |-  ( G e. UMGraph <-> ( G e. UPGraph /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } ) )
8 7 biimpri 
 |-  ( ( G e. UPGraph /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } ) -> G e. UMGraph )
9 6 8 syldan 
 |-  ( ( G e. UPGraph /\ G e. AcyclicGraph ) -> G e. UMGraph )