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∈UMGraph∧A∈V∧B∈V∧C∈V∧AB∈E∧BC∈E∧CA∈E→∃f∃pfCycles⁡Gp∧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∈UMGraph→G∈UHGraph
4 3 3ad2ant1 ⊢G∈UMGraph∧A∈V∧B∈V∧C∈V∧AB∈E∧BC∈E∧CA∈E→G∈UHGraph
5 simp2 ⊢G∈UMGraph∧A∈V∧B∈V∧C∈V∧AB∈E∧BC∈E∧CA∈E→A∈V∧B∈V∧C∈V
6 2 umgredgne ⊢G∈UMGraph∧AB∈E→A≠B
7 6 3ad2antr1 ⊢G∈UMGraph∧AB∈E∧BC∈E∧CA∈E→A≠B
8 prcom ⊢CA=AC
9 8 eleq1i ⊢CA∈E↔AC∈E
10 9 biimpi ⊢CA∈E→AC∈E
11 10 3ad2ant3 ⊢AB∈E∧BC∈E∧CA∈E→AC∈E
12 2 umgredgne ⊢G∈UMGraph∧AC∈E→A≠C
13 11 12 sylan2 ⊢G∈UMGraph∧AB∈E∧BC∈E∧CA∈E→A≠C
14 simp2 ⊢AB∈E∧BC∈E∧CA∈E→BC∈E
15 2 umgredgne ⊢G∈UMGraph∧BC∈E→B≠C
16 14 15 sylan2 ⊢G∈UMGraph∧AB∈E∧BC∈E∧CA∈E→B≠C
17 7 13 16 3jca ⊢G∈UMGraph∧AB∈E∧BC∈E∧CA∈E→A≠B∧A≠C∧B≠C
18 17 3adant2 ⊢G∈UMGraph∧A∈V∧B∈V∧C∈V∧AB∈E∧BC∈E∧CA∈E→A≠B∧A≠C∧B≠C
19 simp3 ⊢G∈UMGraph∧A∈V∧B∈V∧C∈V∧AB∈E∧BC∈E∧CA∈E→AB∈E∧BC∈E∧CA∈E
20 1 2 uhgr3cyclex ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧AB∈E∧BC∈E∧CA∈E→∃f∃pfCycles⁡Gp∧f=3∧p⁡0=A
21 4 5 18 19 20 syl121anc ⊢G∈UMGraph∧A∈V∧B∈V∧C∈V∧AB∈E∧BC∈E∧CA∈E→∃f∃pfCycles⁡Gp∧f=3∧p⁡0=A