Proof of Theorem umgr2cycl
Step | Hyp | Ref
| Expression |
1 | | ax-5 1917 |
. . . . . . 7
⊢ (𝑗 ∈ dom 𝐼 → ∀𝑘 𝑗 ∈ dom 𝐼) |
2 | | alral 3082 |
. . . . . . 7
⊢
(∀𝑘 𝑗 ∈ dom 𝐼 → ∀𝑘 ∈ dom 𝐼 𝑗 ∈ dom 𝐼) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝑗 ∈ dom 𝐼 → ∀𝑘 ∈ dom 𝐼 𝑗 ∈ dom 𝐼) |
4 | | r19.29 3186 |
. . . . . 6
⊢
((∀𝑘 ∈
dom 𝐼 𝑗 ∈ dom 𝐼 ∧ ∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑘 ∈ dom 𝐼(𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘))) |
5 | 3, 4 | sylan 580 |
. . . . 5
⊢ ((𝑗 ∈ dom 𝐼 ∧ ∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑘 ∈ dom 𝐼(𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘))) |
6 | | eqid 2740 |
. . . . . . . . 9
⊢
〈“𝑗𝑘”〉 =
〈“𝑗𝑘”〉 |
7 | | umgr2cycl.1 |
. . . . . . . . 9
⊢ 𝐼 = (iEdg‘𝐺) |
8 | | simp1 1135 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → 𝐺 ∈ UMGraph) |
9 | | simp2 1136 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → 𝑗 ∈ dom 𝐼) |
10 | | simp3r 1201 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → 𝑗 ≠ 𝑘) |
11 | | simp3l 1200 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → (𝐼‘𝑗) = (𝐼‘𝑘)) |
12 | 6, 7, 8, 9, 10, 11 | umgr2cycllem 33098 |
. . . . . . . 8
⊢ ((𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑝〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝) |
13 | | s2len 14600 |
. . . . . . . . 9
⊢
(♯‘〈“𝑗𝑘”〉) = 2 |
14 | 13 | ax-gen 1802 |
. . . . . . . 8
⊢
∀𝑝(♯‘〈“𝑗𝑘”〉) = 2 |
15 | | 19.29r 1881 |
. . . . . . . . 9
⊢
((∃𝑝〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝 ∧ ∀𝑝(♯‘〈“𝑗𝑘”〉) = 2) → ∃𝑝(〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝 ∧ (♯‘〈“𝑗𝑘”〉) = 2)) |
16 | | s2cli 14591 |
. . . . . . . . . . . 12
⊢
〈“𝑗𝑘”〉 ∈ Word
V |
17 | | breq1 5082 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 〈“𝑗𝑘”〉 → (𝑓(Cycles‘𝐺)𝑝 ↔ 〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝)) |
18 | | fveqeq2 6780 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 〈“𝑗𝑘”〉 → ((♯‘𝑓) = 2 ↔
(♯‘〈“𝑗𝑘”〉) = 2)) |
19 | 17, 18 | anbi12d 631 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 〈“𝑗𝑘”〉 → ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2) ↔ (〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝 ∧ (♯‘〈“𝑗𝑘”〉) = 2))) |
20 | 19 | rspcev 3561 |
. . . . . . . . . . . 12
⊢
((〈“𝑗𝑘”〉 ∈ Word V ∧
(〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝 ∧ (♯‘〈“𝑗𝑘”〉) = 2)) → ∃𝑓 ∈ Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |
21 | 16, 20 | mpan 687 |
. . . . . . . . . . 11
⊢
((〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝 ∧ (♯‘〈“𝑗𝑘”〉) = 2) → ∃𝑓 ∈ Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |
22 | | rexex 3170 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2) → ∃𝑓(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
⊢
((〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝 ∧ (♯‘〈“𝑗𝑘”〉) = 2) → ∃𝑓(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |
24 | 23 | eximi 1841 |
. . . . . . . . 9
⊢
(∃𝑝(〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝 ∧ (♯‘〈“𝑗𝑘”〉) = 2) → ∃𝑝∃𝑓(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |
25 | | excomim 2167 |
. . . . . . . . 9
⊢
(∃𝑝∃𝑓(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |
26 | 15, 24, 25 | 3syl 18 |
. . . . . . . 8
⊢
((∃𝑝〈“𝑗𝑘”〉(Cycles‘𝐺)𝑝 ∧ ∀𝑝(♯‘〈“𝑗𝑘”〉) = 2) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |
27 | 12, 14, 26 | sylancl 586 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |
28 | 27 | 3expib 1121 |
. . . . . 6
⊢ (𝐺 ∈ UMGraph → ((𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2))) |
29 | 28 | rexlimdvw 3221 |
. . . . 5
⊢ (𝐺 ∈ UMGraph →
(∃𝑘 ∈ dom 𝐼(𝑗 ∈ dom 𝐼 ∧ ((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2))) |
30 | 5, 29 | syl5 34 |
. . . 4
⊢ (𝐺 ∈ UMGraph → ((𝑗 ∈ dom 𝐼 ∧ ∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2))) |
31 | 30 | expd 416 |
. . 3
⊢ (𝐺 ∈ UMGraph → (𝑗 ∈ dom 𝐼 → (∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)))) |
32 | 31 | rexlimdv 3214 |
. 2
⊢ (𝐺 ∈ UMGraph →
(∃𝑗 ∈ dom 𝐼∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2))) |
33 | 32 | imp 407 |
1
⊢ ((𝐺 ∈ UMGraph ∧
∃𝑗 ∈ dom 𝐼∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2)) |