| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 3anass 1095 | . . . . . . 7
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) | 
| 2 | 1 | bianass 642 | . . . . . 6
⊢ ((𝐺 ∈ ComplUSGraph ∧
(𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ↔ ((𝐺 ∈ ComplUSGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) | 
| 3 |  | cusgrusgr 29436 | . . . . . . . . 9
⊢ (𝐺 ∈ ComplUSGraph →
𝐺 ∈
USGraph) | 
| 4 |  | usgrumgr 29198 | . . . . . . . . 9
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UMGraph) | 
| 5 | 3, 4 | syl 17 | . . . . . . . 8
⊢ (𝐺 ∈ ComplUSGraph →
𝐺 ∈
UMGraph) | 
| 6 |  | 3simpc 1151 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) | 
| 7 | 6 | ancli 548 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) | 
| 8 |  | df-3an 1089 | . . . . . . . . . . . . 13
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐) ∧ 𝑏 ≠ 𝑐)) | 
| 9 | 8 | biimpi 216 | . . . . . . . . . . . 12
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) → ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐) ∧ 𝑏 ≠ 𝑐)) | 
| 10 |  | an32 646 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ↔ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) | 
| 11 | 10 | anbi1i 624 | . . . . . . . . . . . . . 14
⊢
(((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ 𝑏 ≠ 𝑐) ↔ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑏 ≠ 𝑐)) | 
| 12 |  | anass 468 | . . . . . . . . . . . . . 14
⊢
(((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑏 ≠ 𝑐) ↔ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑏 ≠ 𝑐))) | 
| 13 | 11, 12 | sylbb 219 | . . . . . . . . . . . . 13
⊢
(((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ 𝑏 ≠ 𝑐) → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑏 ≠ 𝑐))) | 
| 14 | 13 | anasss 466 | . . . . . . . . . . . 12
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐) ∧ 𝑏 ≠ 𝑐)) → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑏 ≠ 𝑐))) | 
| 15 | 7, 9, 14 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑏 ≠ 𝑐))) | 
| 16 |  | anandi3 1102 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) | 
| 17 | 16 | anbi1i 624 | . . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ↔ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐))) | 
| 18 |  | an4 656 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ↔ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) ∧ ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑎 ≠ 𝑐))) | 
| 19 | 17, 18 | sylbb 219 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) ∧ ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑎 ≠ 𝑐))) | 
| 20 |  | df-3an 1089 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏)) | 
| 21 |  | cusgr3cyclex.1 | . . . . . . . . . . . . . . . 16
⊢ 𝑉 = (Vtx‘𝐺) | 
| 22 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(Edg‘𝐺) =
(Edg‘𝐺) | 
| 23 | 21, 22 | cusgredgex2 35128 | . . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ ComplUSGraph →
((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ (Edg‘𝐺))) | 
| 24 | 20, 23 | biimtrrid 243 | . . . . . . . . . . . . . 14
⊢ (𝐺 ∈ ComplUSGraph →
(((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → {𝑎, 𝑏} ∈ (Edg‘𝐺))) | 
| 25 |  | df-3an 1089 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐) ↔ ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑎 ≠ 𝑐)) | 
| 26 | 21, 22 | cusgredgex2 35128 | . . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ ComplUSGraph →
((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐) → {𝑎, 𝑐} ∈ (Edg‘𝐺))) | 
| 27 | 25, 26 | biimtrrid 243 | . . . . . . . . . . . . . 14
⊢ (𝐺 ∈ ComplUSGraph →
(((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑎 ≠ 𝑐) → {𝑎, 𝑐} ∈ (Edg‘𝐺))) | 
| 28 | 24, 27 | anim12d 609 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ ComplUSGraph →
((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) ∧ ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑎 ≠ 𝑐)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)))) | 
| 29 | 19, 28 | syl5 34 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ ComplUSGraph →
(((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)))) | 
| 30 |  | df-3an 1089 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ↔ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑏 ≠ 𝑐)) | 
| 31 | 21, 22 | cusgredgex2 35128 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ ComplUSGraph →
((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → {𝑏, 𝑐} ∈ (Edg‘𝐺))) | 
| 32 | 30, 31 | biimtrrid 243 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ ComplUSGraph →
(((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑏 ≠ 𝑐) → {𝑏, 𝑐} ∈ (Edg‘𝐺))) | 
| 33 | 29, 32 | anim12d 609 | . . . . . . . . . . 11
⊢ (𝐺 ∈ ComplUSGraph →
((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐)) ∧ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ 𝑏 ≠ 𝑐)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) | 
| 34 | 15, 33 | syl5 34 | . . . . . . . . . 10
⊢ (𝐺 ∈ ComplUSGraph →
(((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) | 
| 35 |  | 3anan32 1097 | . . . . . . . . . . 11
⊢ (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) ↔ (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) | 
| 36 |  | prcom 4732 | . . . . . . . . . . . . 13
⊢ {𝑎, 𝑐} = {𝑐, 𝑎} | 
| 37 | 36 | eleq1i 2832 | . . . . . . . . . . . 12
⊢ ({𝑎, 𝑐} ∈ (Edg‘𝐺) ↔ {𝑐, 𝑎} ∈ (Edg‘𝐺)) | 
| 38 | 37 | 3anbi3i 1160 | . . . . . . . . . . 11
⊢ (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) ↔ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) | 
| 39 | 35, 38 | bitr3i 277 | . . . . . . . . . 10
⊢ ((({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) | 
| 40 | 34, 39 | imbitrdi 251 | . . . . . . . . 9
⊢ (𝐺 ∈ ComplUSGraph →
(((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺)))) | 
| 41 |  | pm5.3 572 | . . . . . . . . 9
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) ↔ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))))) | 
| 42 | 40, 41 | sylib 218 | . . . . . . . 8
⊢ (𝐺 ∈ ComplUSGraph →
(((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))))) | 
| 43 | 21, 22 | umgr3cyclex 30202 | . . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝑎)) | 
| 44 |  | 3simpa 1149 | . . . . . . . . . . 11
⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝑎) → (𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) | 
| 45 | 44 | 2eximi 1836 | . . . . . . . . . 10
⊢
(∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝑎) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) | 
| 46 | 43, 45 | syl 17 | . . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) | 
| 47 | 46 | 3expib 1123 | . . . . . . . 8
⊢ (𝐺 ∈ UMGraph → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))) | 
| 48 | 5, 42, 47 | sylsyld 61 | . . . . . . 7
⊢ (𝐺 ∈ ComplUSGraph →
(((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))) | 
| 49 | 48 | expdimp 452 | . . . . . 6
⊢ ((𝐺 ∈ ComplUSGraph ∧
(𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))) | 
| 50 | 2, 49 | sylbir 235 | . . . . 5
⊢ (((𝐺 ∈ ComplUSGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))) | 
| 51 | 50 | reximdvva 3207 | . . . 4
⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))) | 
| 52 | 51 | reximdva 3168 | . . 3
⊢ (𝐺 ∈ ComplUSGraph →
(∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))) | 
| 53 |  | id 22 | . . . . . 6
⊢
(∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) | 
| 54 | 53 | rexlimivw 3151 | . . . . 5
⊢
(∃𝑐 ∈
𝑉 ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) | 
| 55 | 54 | rexlimivw 3151 | . . . 4
⊢
(∃𝑏 ∈
𝑉 ∃𝑐 ∈ 𝑉 ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) | 
| 56 | 55 | rexlimivw 3151 | . . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) | 
| 57 | 52, 56 | syl6 35 | . 2
⊢ (𝐺 ∈ ComplUSGraph →
(∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))) | 
| 58 | 21 | fvexi 6920 | . . 3
⊢ 𝑉 ∈ V | 
| 59 |  | hashgt23el 14463 | . . 3
⊢ ((𝑉 ∈ V ∧ 2 <
(♯‘𝑉)) →
∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 60 | 58, 59 | mpan 690 | . 2
⊢ (2 <
(♯‘𝑉) →
∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 61 | 57, 60 | impel 505 | 1
⊢ ((𝐺 ∈ ComplUSGraph ∧ 2
< (♯‘𝑉))
→ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3)) |