Metamath Proof Explorer

Theorem umgr2cycl

Description: A multigraph with two distinct edges that connect the same vertices has a 2-cycle. (Contributed by BTernaryTau, 17-Oct-2023)

Ref Expression
Hypothesis umgr2cycl.1 
|- I = ( iEdg ` G )
Assertion umgr2cycl 
|- ( ( G e. UMGraph /\ E. j e. dom I E. k e. dom I ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )

Proof

Step Hyp Ref Expression
1 umgr2cycl.1 
 |-  I = ( iEdg ` G )
2 ax-5 
 |-  ( j e. dom I -> A. k j e. dom I )
3 alral 
 |-  ( A. k j e. dom I -> A. k e. dom I j e. dom I )
4 2 3 syl 
 |-  ( j e. dom I -> A. k e. dom I j e. dom I )
5 r19.29 
 |-  ( ( A. k e. dom I j e. dom I /\ E. k e. dom I ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. k e. dom I ( j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) )
6 4 5 sylan 
 |-  ( ( j e. dom I /\ E. k e. dom I ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. k e. dom I ( j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) )
7 eqid 
 |-  <" j k "> = <" j k ">
8 simp1 
 |-  ( ( G e. UMGraph /\ j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> G e. UMGraph )
9 simp2 
 |-  ( ( G e. UMGraph /\ j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> j e. dom I )
10 simp3r 
 |-  ( ( G e. UMGraph /\ j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> j =/= k )
11 simp3l 
 |-  ( ( G e. UMGraph /\ j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> ( I ` j ) = ( I ` k ) )
12 7 1 8 9 10 11 umgr2cycllem 
 |-  ( ( G e. UMGraph /\ j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. p <" j k "> ( Cycles ` G ) p )
13 s2len 
 |-  ( # ` <" j k "> ) = 2
14 13 ax-gen 
 |-  A. p ( # ` <" j k "> ) = 2
15 19.29r 
 |-  ( ( E. p <" j k "> ( Cycles ` G ) p /\ A. p ( # ` <" j k "> ) = 2 ) -> E. p ( <" j k "> ( Cycles ` G ) p /\ ( # ` <" j k "> ) = 2 ) )
16 s2cli 
 |-  <" j k "> e. Word _V
17 breq1 
 |-  ( f = <" j k "> -> ( f ( Cycles ` G ) p <-> <" j k "> ( Cycles ` G ) p ) )
18 fveqeq2 
 |-  ( f = <" j k "> -> ( ( # ` f ) = 2 <-> ( # ` <" j k "> ) = 2 ) )
19 17 18 anbi12d 
 |-  ( f = <" j k "> -> ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) <-> ( <" j k "> ( Cycles ` G ) p /\ ( # ` <" j k "> ) = 2 ) ) )
20 19 rspcev 
 |-  ( ( <" j k "> e. Word _V /\ ( <" j k "> ( Cycles ` G ) p /\ ( # ` <" j k "> ) = 2 ) ) -> E. f e. Word _V ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
21 16 20 mpan 
 |-  ( ( <" j k "> ( Cycles ` G ) p /\ ( # ` <" j k "> ) = 2 ) -> E. f e. Word _V ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
22 rexex 
 |-  ( E. f e. Word _V ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) -> E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
23 21 22 syl 
 |-  ( ( <" j k "> ( Cycles ` G ) p /\ ( # ` <" j k "> ) = 2 ) -> E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
24 23 eximi 
 |-  ( E. p ( <" j k "> ( Cycles ` G ) p /\ ( # ` <" j k "> ) = 2 ) -> E. p E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
25 excomim 
 |-  ( E. p E. f ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
26 15 24 25 3syl 
 |-  ( ( E. p <" j k "> ( Cycles ` G ) p /\ A. p ( # ` <" j k "> ) = 2 ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
27 12 14 26 sylancl 
 |-  ( ( G e. UMGraph /\ j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
28 27 3expib 
 |-  ( G e. UMGraph -> ( ( j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) ) )
29 28 rexlimdvw 
 |-  ( G e. UMGraph -> ( E. k e. dom I ( j e. dom I /\ ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) ) )
30 6 29 syl5 
 |-  ( G e. UMGraph -> ( ( j e. dom I /\ E. k e. dom I ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) ) )
31 30 expd 
 |-  ( G e. UMGraph -> ( j e. dom I -> ( E. k e. dom I ( ( I ` j ) = ( I ` k ) /\ j =/= k ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) ) ) )
32 31 rexlimdv 
 |-  ( G e. UMGraph -> ( E. j e. dom I E. k e. dom I ( ( I ` j ) = ( I ` k ) /\ j =/= k ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) ) )
33 32 imp 
 |-  ( ( G e. UMGraph /\ E. j e. dom I E. k e. dom I ( ( I ` j ) = ( I ` k ) /\ j =/= k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )