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 𝑉 = ( Vtx ‘ 𝐺 )
uhgr3cyclex.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgr3v3e3cycl ( 𝐺 ∈ UMGraph → ( ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ↔ ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v 𝑉 = ( Vtx ‘ 𝐺 )
2 uhgr3cyclex.e 𝐸 = ( Edg ‘ 𝐺 )
3 umgrupgr ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph )
4 3 adantr ( ( 𝐺 ∈ UMGraph ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) → 𝐺 ∈ UPGraph )
5 simpl ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 )
6 5 adantl ( ( 𝐺 ∈ UMGraph ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) → 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 )
7 simpr ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ( ♯ ‘ 𝑓 ) = 3 )
8 7 adantl ( ( 𝐺 ∈ UMGraph ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) → ( ♯ ‘ 𝑓 ) = 3 )
9 2 1 upgr3v3e3cycl ( ( 𝐺 ∈ UPGraph ∧ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎𝑏𝑏𝑐𝑐𝑎 ) ) )
10 simpl ( ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎𝑏𝑏𝑐𝑐𝑎 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
11 10 reximi ( ∃ 𝑐𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎𝑏𝑏𝑐𝑐𝑎 ) ) → ∃ 𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
12 11 reximi ( ∃ 𝑏𝑉𝑐𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎𝑏𝑏𝑐𝑐𝑎 ) ) → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
13 12 reximi ( ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑎𝑏𝑏𝑐𝑐𝑎 ) ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
14 9 13 syl ( ( 𝐺 ∈ UPGraph ∧ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
15 4 6 8 14 syl3anc ( ( 𝐺 ∈ UMGraph ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
16 15 ex ( 𝐺 ∈ UMGraph → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )
17 16 exlimdvv ( 𝐺 ∈ UMGraph → ( ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )
18 simplll ( ( ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ 𝑐𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → 𝐺 ∈ UMGraph )
19 df-3an ( ( 𝑎𝑉𝑏𝑉𝑐𝑉 ) ↔ ( ( 𝑎𝑉𝑏𝑉 ) ∧ 𝑐𝑉 ) )
20 19 biimpri ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ 𝑐𝑉 ) → ( 𝑎𝑉𝑏𝑉𝑐𝑉 ) )
21 20 ad4ant23 ( ( ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ 𝑐𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ( 𝑎𝑉𝑏𝑉𝑐𝑉 ) )
22 simpr ( ( ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ 𝑐𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
23 1 2 umgr3cyclex ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎𝑉𝑏𝑉𝑐𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) )
24 3simpa ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
25 24 2eximi ( ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) → ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
26 23 25 syl ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎𝑉𝑏𝑉𝑐𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
27 18 21 22 26 syl3anc ( ( ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ 𝑐𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
28 27 rexlimdva2 ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( ∃ 𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
29 28 rexlimdvva ( 𝐺 ∈ UMGraph → ( ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
30 17 29 impbid ( 𝐺 ∈ UMGraph → ( ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ↔ ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )