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 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )