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 )