Metamath Proof Explorer


Theorem umgr3v3e3cycl

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

Ref Expression
Hypotheses uhgr3cyclex.v V = Vtx G
uhgr3cyclex.e E = Edg G
Assertion umgr3v3e3cycl G UMGraph f p f Cycles G p f = 3 a V b V c V a b E b c E c a E

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v V = Vtx G
2 uhgr3cyclex.e E = Edg G
3 umgrupgr G UMGraph G UPGraph
4 3 adantr G UMGraph f Cycles G p f = 3 G UPGraph
5 simpl f Cycles G p f = 3 f Cycles G p
6 5 adantl G UMGraph f Cycles G p f = 3 f Cycles G p
7 simpr f Cycles G p f = 3 f = 3
8 7 adantl G UMGraph f Cycles G p f = 3 f = 3
9 2 1 upgr3v3e3cycl G UPGraph f Cycles G p f = 3 a V b V c V a b E b c E c a E a b b c c a
10 simpl a b E b c E c a E a b b c c a a b E b c E c a E
11 10 reximi c V a b E b c E c a E a b b c c a c V a b E b c E c a E
12 11 reximi b V c V a b E b c E c a E a b b c c a b V c V a b E b c E c a E
13 12 reximi a V b V c V a b E b c E c a E a b b c c a a V b V c V a b E b c E c a E
14 9 13 syl G UPGraph f Cycles G p f = 3 a V b V c V a b E b c E c a E
15 4 6 8 14 syl3anc G UMGraph f Cycles G p f = 3 a V b V c V a b E b c E c a E
16 15 ex G UMGraph f Cycles G p f = 3 a V b V c V a b E b c E c a E
17 16 exlimdvv G UMGraph f p f Cycles G p f = 3 a V b V c V a b E b c E c a E
18 simplll G UMGraph a V b V c V a b E b c E c a E G UMGraph
19 df-3an a V b V c V a V b V c V
20 19 biimpri a V b V c V a V b V c V
21 20 ad4ant23 G UMGraph a V b V c V a b E b c E c a E a V b V c V
22 simpr G UMGraph a V b V c V a b E b c E c a E a b E b c E c a E
23 1 2 umgr3cyclex G UMGraph a V b V c V a b E b c E c a E f p f Cycles G p f = 3 p 0 = a
24 3simpa f Cycles G p f = 3 p 0 = a f Cycles G p f = 3
25 24 2eximi f p f Cycles G p f = 3 p 0 = a f p f Cycles G p f = 3
26 23 25 syl G UMGraph a V b V c V a b E b c E c a E f p f Cycles G p f = 3
27 18 21 22 26 syl3anc G UMGraph a V b V c V a b E b c E c a E f p f Cycles G p f = 3
28 27 rexlimdva2 G UMGraph a V b V c V a b E b c E c a E f p f Cycles G p f = 3
29 28 rexlimdvva G UMGraph a V b V c V a b E b c E c a E f p f Cycles G p f = 3
30 17 29 impbid G UMGraph f p f Cycles G p f = 3 a V b V c V a b E b c E c a E