Metamath Proof Explorer

Theorem cusgr3cyclex

Description: Every complete simple graph with more than two vertices has a 3-cycle. (Contributed by BTernaryTau, 4-Oct-2023)

Ref Expression
Hypothesis cusgr3cyclex.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion cusgr3cyclex ( ( 𝐺 ∈ ComplUSGraph ∧ 2 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )

Proof

Step Hyp Ref Expression
1 cusgr3cyclex.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 3anass ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ↔ ( 𝑎 ∈ 𝑉 ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
3 2 bianass ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ↔ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
4 cusgrusgr ⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph )
5 usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
6 4 5 syl ⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ UMGraph )
7 3simpc ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) )
8 7 ancli ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
9 df-3an ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ∧ 𝑏 ≠ 𝑐 ) )
10 9 biimpi ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ∧ 𝑏 ≠ 𝑐 ) )
11 an32 ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ↔ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
12 11 anbi1i ⊢ ( ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ 𝑏 ≠ 𝑐 ) ↔ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑏 ≠ 𝑐 ) )
13 anass ⊢ ( ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑏 ≠ 𝑐 ) ↔ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑏 ≠ 𝑐 ) ) )
14 12 13 sylbb ⊢ ( ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ 𝑏 ≠ 𝑐 ) → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑏 ≠ 𝑐 ) ) )
15 14 anasss ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ∧ 𝑏 ≠ 𝑐 ) ) → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑏 ≠ 𝑐 ) ) )
16 8 10 15 syl2an ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑏 ≠ 𝑐 ) ) )
17 anandi3 ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
18 17 anbi1i ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ↔ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) )
19 an4 ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ↔ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑐 ) ) )
20 18 19 sylbb ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑐 ) ) )
21 df-3an ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) )
22 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
23 1 22 cusgredgex2 ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) )
24 21 23 syl5bir ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) → { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) )
25 df-3an ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑐 ) )
26 1 22 cusgredgex2 ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ) → { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
27 25 26 syl5bir ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑐 ) → { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
28 24 27 anim12d ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ) ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑐 ) ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
29 20 28 syl5 ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
30 df-3an ⊢ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐 ) ↔ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑏 ≠ 𝑐 ) )
31 1 22 cusgredgex2 ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐 ) → { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
32 30 31 syl5bir ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑏 ≠ 𝑐 ) → { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
33 29 32 anim12d ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ) ) ∧ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ 𝑏 ≠ 𝑐 ) ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
34 16 33 syl5 ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
35 3anan32 ⊢ ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
36 prcom ⊢ { 𝑎 , 𝑐 } = { 𝑐 , 𝑎 }
37 36 eleq1i ⊢ ( { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
38 37 3anbi3i ⊢ ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
39 35 38 bitr3i ⊢ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
40 34 39 syl6ib ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) )
41 pm5.3 ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
42 40 41 sylib ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
43 1 22 umgr3cyclex ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) )
44 3simpa ⊢ ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
45 44 2eximi ⊢ ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
46 43 45 syl ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
47 46 3expib ⊢ ( 𝐺 ∈ UMGraph → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
48 6 42 47 sylsyld ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
49 48 expdimp ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
50 3 49 sylbir ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
51 50 reximdvva ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
52 51 reximdva ⊢ ( 𝐺 ∈ ComplUSGraph → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
53 id ⊢ ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
54 53 rexlimivw ⊢ ( ∃ 𝑐 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
55 54 rexlimivw ⊢ ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
56 55 rexlimivw ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )
57 52 56 syl6 ⊢ ( 𝐺 ∈ ComplUSGraph → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) ) )
58 1 fvexi ⊢ 𝑉 ∈ V
59 hashgt23el ⊢ ( ( 𝑉 ∈ V ∧ 2 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
60 58 59 mpan ⊢ ( 2 < ( ♯ ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
61 57 60 impel ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 2 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ) )