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

Metamath Proof Explorer

Theorem umgrn1cycl

Description: In a multigraph graph (with no loops!) there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017) (Revised by AV, 2-Feb-2021)

Ref Expression
Assertion umgrn1cycl 
|- ( ( G e. UMGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 1 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 umgrislfupgr 
 |-  ( G e. UMGraph <-> ( G e. UPGraph /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } ) )
4 1 2 lfgrn1cycl 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } -> ( F ( Cycles ` G ) P -> ( # ` F ) =/= 1 ) )
5 3 4 simplbiim 
 |-  ( G e. UMGraph -> ( F ( Cycles ` G ) P -> ( # ` F ) =/= 1 ) )
6 5 imp 
 |-  ( ( G e. UMGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 1 )