Metamath Proof Explorer

Theorem umgr3cyclex

Description: If there are three (different) vertices in a multigraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017) (Revised by AV, 12-Feb-2021)

Ref Expression
Hypotheses uhgr3cyclex.v 
|- V = ( Vtx ` G )
uhgr3cyclex.e 
|- E = ( Edg ` G )
Assertion umgr3cyclex 
|- ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v 
 |-  V = ( Vtx ` G )
2 uhgr3cyclex.e 
 |-  E = ( Edg ` G )
3 umgruhgr 
 |-  ( G e. UMGraph -> G e. UHGraph )
4 3 3ad2ant1 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> G e. UHGraph )
5 simp2 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( A e. V /\ B e. V /\ C e. V ) )
6 2 umgredgne 
 |-  ( ( G e. UMGraph /\ { A , B } e. E ) -> A =/= B )
7 6 3ad2antr1 
 |-  ( ( G e. UMGraph /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> A =/= B )
8 prcom 
 |-  { C , A } = { A , C }
9 8 eleq1i 
 |-  ( { C , A } e. E <-> { A , C } e. E )
10 9 biimpi 
 |-  ( { C , A } e. E -> { A , C } e. E )
11 10 3ad2ant3 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> { A , C } e. E )
12 2 umgredgne 
 |-  ( ( G e. UMGraph /\ { A , C } e. E ) -> A =/= C )
13 11 12 sylan2 
 |-  ( ( G e. UMGraph /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> A =/= C )
14 simp2 
 |-  ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> { B , C } e. E )
15 2 umgredgne 
 |-  ( ( G e. UMGraph /\ { B , C } e. E ) -> B =/= C )
16 14 15 sylan2 
 |-  ( ( G e. UMGraph /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> B =/= C )
17 7 13 16 3jca 
 |-  ( ( G e. UMGraph /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( A =/= B /\ A =/= C /\ B =/= C ) )
18 17 3adant2 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( A =/= B /\ A =/= C /\ B =/= C ) )
19 simp3 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) )
20 1 2 uhgr3cyclex 
 |-  ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )
21 4 5 18 19 20 syl121anc 
 |-  ( ( G e. UMGraph /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )