| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | umgr2cycllem.3 | . . 3
⊢ (𝜑 → 𝐺 ∈ UMGraph) | 
| 2 |  | umgruhgr 29122 | . . . . 5
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UHGraph) | 
| 3 |  | umgr2cycllem.2 | . . . . . 6
⊢ 𝐼 = (iEdg‘𝐺) | 
| 4 | 3 | uhgrfun 29084 | . . . . 5
⊢ (𝐺 ∈ UHGraph → Fun 𝐼) | 
| 5 | 1, 2, 4 | 3syl 18 | . . . 4
⊢ (𝜑 → Fun 𝐼) | 
| 6 |  | umgr2cycllem.4 | . . . 4
⊢ (𝜑 → 𝐽 ∈ dom 𝐼) | 
| 7 | 3 | iedgedg 29068 | . . . 4
⊢ ((Fun
𝐼 ∧ 𝐽 ∈ dom 𝐼) → (𝐼‘𝐽) ∈ (Edg‘𝐺)) | 
| 8 | 5, 6, 7 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐼‘𝐽) ∈ (Edg‘𝐺)) | 
| 9 |  | eqid 2736 | . . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 10 |  | eqid 2736 | . . . 4
⊢
(Edg‘𝐺) =
(Edg‘𝐺) | 
| 11 | 9, 10 | umgredg 29156 | . . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐼‘𝐽) ∈ (Edg‘𝐺)) → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) | 
| 12 | 1, 8, 11 | syl2anc 584 | . 2
⊢ (𝜑 → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) | 
| 13 |  | ax-5 1909 | . . . . . . 7
⊢ (𝑎 ∈ (Vtx‘𝐺) → ∀𝑏 𝑎 ∈ (Vtx‘𝐺)) | 
| 14 |  | alral 3074 | . . . . . . 7
⊢
(∀𝑏 𝑎 ∈ (Vtx‘𝐺) → ∀𝑏 ∈ (Vtx‘𝐺)𝑎 ∈ (Vtx‘𝐺)) | 
| 15 | 13, 14 | syl 17 | . . . . . 6
⊢ (𝑎 ∈ (Vtx‘𝐺) → ∀𝑏 ∈ (Vtx‘𝐺)𝑎 ∈ (Vtx‘𝐺)) | 
| 16 |  | r19.29 3113 | . . . . . 6
⊢
((∀𝑏 ∈
(Vtx‘𝐺)𝑎 ∈ (Vtx‘𝐺) ∧ ∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → ∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ∈ (Vtx‘𝐺) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏}))) | 
| 17 | 15, 16 | sylan 580 | . . . . 5
⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ ∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → ∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ∈ (Vtx‘𝐺) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏}))) | 
| 18 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
〈“𝑎𝑏𝑎”〉 = 〈“𝑎𝑏𝑎”〉 | 
| 19 |  | umgr2cycllem.1 | . . . . . . . . . . . 12
⊢ 𝐹 = 〈“𝐽𝐾”〉 | 
| 20 |  | simp2 1137 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺))) | 
| 21 |  | simp3l 1201 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → 𝑎 ≠ 𝑏) | 
| 22 |  | eqimss2 4042 | . . . . . . . . . . . . . . 15
⊢ ((𝐼‘𝐽) = {𝑎, 𝑏} → {𝑎, 𝑏} ⊆ (𝐼‘𝐽)) | 
| 23 | 22 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏}) → {𝑎, 𝑏} ⊆ (𝐼‘𝐽)) | 
| 24 | 23 | 3ad2ant3 1135 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → {𝑎, 𝑏} ⊆ (𝐼‘𝐽)) | 
| 25 |  | umgr2cycllem.6 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐼‘𝐽) = (𝐼‘𝐾)) | 
| 26 | 25 | sseq2d 4015 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ({𝑎, 𝑏} ⊆ (𝐼‘𝐽) ↔ {𝑎, 𝑏} ⊆ (𝐼‘𝐾))) | 
| 27 | 22, 26 | imbitrid 244 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐼‘𝐽) = {𝑎, 𝑏} → {𝑎, 𝑏} ⊆ (𝐼‘𝐾))) | 
| 28 | 27 | adantld 490 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏}) → {𝑎, 𝑏} ⊆ (𝐼‘𝐾))) | 
| 29 | 28 | adantld 490 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → {𝑎, 𝑏} ⊆ (𝐼‘𝐾))) | 
| 30 | 29 | 3impib 1116 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → {𝑎, 𝑏} ⊆ (𝐼‘𝐾)) | 
| 31 | 24, 30 | jca 511 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → ({𝑎, 𝑏} ⊆ (𝐼‘𝐽) ∧ {𝑎, 𝑏} ⊆ (𝐼‘𝐾))) | 
| 32 |  | umgr2cycllem.5 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ≠ 𝐾) | 
| 33 | 32 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → 𝐽 ≠ 𝐾) | 
| 34 | 18, 19, 20, 21, 31, 9, 3, 33 | 2cycl2d 35145 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → 𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉) | 
| 35 | 34 | 3expib 1122 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → 𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉)) | 
| 36 | 35 | exp4c 432 | . . . . . . . . 9
⊢ (𝜑 → (𝑎 ∈ (Vtx‘𝐺) → (𝑏 ∈ (Vtx‘𝐺) → ((𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏}) → 𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉)))) | 
| 37 | 36 | com23 86 | . . . . . . . 8
⊢ (𝜑 → (𝑏 ∈ (Vtx‘𝐺) → (𝑎 ∈ (Vtx‘𝐺) → ((𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏}) → 𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉)))) | 
| 38 | 37 | imp4a 422 | . . . . . . 7
⊢ (𝜑 → (𝑏 ∈ (Vtx‘𝐺) → ((𝑎 ∈ (Vtx‘𝐺) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → 𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉))) | 
| 39 |  | s3cli 14921 | . . . . . . . . 9
⊢
〈“𝑎𝑏𝑎”〉 ∈ Word V | 
| 40 |  | breq2 5146 | . . . . . . . . . 10
⊢ (𝑝 = 〈“𝑎𝑏𝑎”〉 → (𝐹(Cycles‘𝐺)𝑝 ↔ 𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉)) | 
| 41 | 40 | rspcev 3621 | . . . . . . . . 9
⊢
((〈“𝑎𝑏𝑎”〉 ∈ Word V ∧ 𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉) → ∃𝑝 ∈ Word V𝐹(Cycles‘𝐺)𝑝) | 
| 42 | 39, 41 | mpan 690 | . . . . . . . 8
⊢ (𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉 → ∃𝑝 ∈ Word V𝐹(Cycles‘𝐺)𝑝) | 
| 43 |  | rexex 3075 | . . . . . . . 8
⊢
(∃𝑝 ∈
Word V𝐹(Cycles‘𝐺)𝑝 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝) | 
| 44 | 42, 43 | syl 17 | . . . . . . 7
⊢ (𝐹(Cycles‘𝐺)〈“𝑎𝑏𝑎”〉 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝) | 
| 45 | 38, 44 | syl8 76 | . . . . . 6
⊢ (𝜑 → (𝑏 ∈ (Vtx‘𝐺) → ((𝑎 ∈ (Vtx‘𝐺) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → ∃𝑝 𝐹(Cycles‘𝐺)𝑝))) | 
| 46 | 45 | rexlimdv 3152 | . . . . 5
⊢ (𝜑 → (∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ∈ (Vtx‘𝐺) ∧ (𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → ∃𝑝 𝐹(Cycles‘𝐺)𝑝)) | 
| 47 | 17, 46 | syl5 34 | . . . 4
⊢ (𝜑 → ((𝑎 ∈ (Vtx‘𝐺) ∧ ∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏})) → ∃𝑝 𝐹(Cycles‘𝐺)𝑝)) | 
| 48 | 47 | expd 415 | . . 3
⊢ (𝜑 → (𝑎 ∈ (Vtx‘𝐺) → (∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏}) → ∃𝑝 𝐹(Cycles‘𝐺)𝑝))) | 
| 49 | 48 | rexlimdv 3152 | . 2
⊢ (𝜑 → (∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)(𝑎 ≠ 𝑏 ∧ (𝐼‘𝐽) = {𝑎, 𝑏}) → ∃𝑝 𝐹(Cycles‘𝐺)𝑝)) | 
| 50 | 12, 49 | mpd 15 | 1
⊢ (𝜑 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝) |