| Step | Hyp | Ref
| Expression |
| 1 | | wlkv 29630 |
. . . . 5
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
| 2 | | simp3l 1202 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝐹(Walks‘𝐺)𝑃 ∧ (Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)))) → Fun (iEdg‘𝐺)) |
| 3 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝐹(Walks‘𝐺)𝑃 ∧ (Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)))) → 𝐹(Walks‘𝐺)𝑃) |
| 4 | | c0ex 11255 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
| 5 | 4 | snid 4662 |
. . . . . . . . . . . 12
⊢ 0 ∈
{0} |
| 6 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹) =
1 → (0..^(♯‘𝐹)) = (0..^1)) |
| 7 | | fzo01 13786 |
. . . . . . . . . . . . 13
⊢ (0..^1) =
{0} |
| 8 | 6, 7 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
1 → (0..^(♯‘𝐹)) = {0}) |
| 9 | 5, 8 | eleqtrrid 2848 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
1 → 0 ∈ (0..^(♯‘𝐹))) |
| 10 | 9 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((Fun
(iEdg‘𝐺) ∧
((♯‘𝐹) = 1
∧ (𝑃‘0) = (𝑃‘1))) → 0 ∈
(0..^(♯‘𝐹))) |
| 11 | 10 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝐹(Walks‘𝐺)𝑃 ∧ (Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)))) → 0 ∈
(0..^(♯‘𝐹))) |
| 12 | | eqid 2737 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 13 | 12 | iedginwlk 29655 |
. . . . . . . . 9
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐹(Walks‘𝐺)𝑃 ∧ 0 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘0)) ∈ ran (iEdg‘𝐺)) |
| 14 | 2, 3, 11, 13 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝐹(Walks‘𝐺)𝑃 ∧ (Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)))) → ((iEdg‘𝐺)‘(𝐹‘0)) ∈ ran (iEdg‘𝐺)) |
| 15 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 16 | 15, 12 | iswlkg 29631 |
. . . . . . . . . 10
⊢ (𝐺 ∈ V → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
| 17 | 8 | raleqdv 3326 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹) =
1 → (∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ↔ ∀𝑘 ∈ {0}if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) |
| 18 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
| 19 | | 0p1e1 12388 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
| 20 | 18, 19 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
| 21 | | wkslem2 29626 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 = 0 ∧ (𝑘 + 1) = 1) → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ↔ if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0))))) |
| 22 | 20, 21 | mpdan 687 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ↔ if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0))))) |
| 23 | 4, 22 | ralsn 4681 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
{0}if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ↔ if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0)))) |
| 24 | 17, 23 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹) =
1 → (∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ↔ if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0))))) |
| 25 | 24 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((Fun
(iEdg‘𝐺) ∧
((♯‘𝐹) = 1
∧ (𝑃‘0) = (𝑃‘1))) →
(∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ↔ if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0))))) |
| 26 | | ifptru 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘0) = (𝑃‘1) → (if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0))) ↔ ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)})) |
| 27 | 26 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃‘0) = (𝑃‘1) ∧ if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0)))) → ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}) |
| 28 | 27 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃‘0) = (𝑃‘1) ∧ if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0)))) → {(𝑃‘0)} = ((iEdg‘𝐺)‘(𝐹‘0))) |
| 29 | 28 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘0) = (𝑃‘1) → (if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0))) → {(𝑃‘0)} = ((iEdg‘𝐺)‘(𝐹‘0)))) |
| 30 | 29 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((Fun
(iEdg‘𝐺) ∧
((♯‘𝐹) = 1
∧ (𝑃‘0) = (𝑃‘1))) → (if-((𝑃‘0) = (𝑃‘1), ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ ((iEdg‘𝐺)‘(𝐹‘0))) → {(𝑃‘0)} = ((iEdg‘𝐺)‘(𝐹‘0)))) |
| 31 | 25, 30 | sylbid 240 |
. . . . . . . . . . . 12
⊢ ((Fun
(iEdg‘𝐺) ∧
((♯‘𝐹) = 1
∧ (𝑃‘0) = (𝑃‘1))) →
(∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → {(𝑃‘0)} = ((iEdg‘𝐺)‘(𝐹‘0)))) |
| 32 | 31 | com12 32 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ((Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} = ((iEdg‘𝐺)‘(𝐹‘0)))) |
| 33 | 32 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} = ((iEdg‘𝐺)‘(𝐹‘0)))) |
| 34 | 16, 33 | biimtrdi 253 |
. . . . . . . . 9
⊢ (𝐺 ∈ V → (𝐹(Walks‘𝐺)𝑃 → ((Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} = ((iEdg‘𝐺)‘(𝐹‘0))))) |
| 35 | 34 | 3imp 1111 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝐹(Walks‘𝐺)𝑃 ∧ (Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)))) → {(𝑃‘0)} = ((iEdg‘𝐺)‘(𝐹‘0))) |
| 36 | | edgval 29066 |
. . . . . . . . 9
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
| 37 | 36 | a1i 11 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝐹(Walks‘𝐺)𝑃 ∧ (Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)))) → (Edg‘𝐺) = ran (iEdg‘𝐺)) |
| 38 | 14, 35, 37 | 3eltr4d 2856 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝐹(Walks‘𝐺)𝑃 ∧ (Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)))) → {(𝑃‘0)} ∈ (Edg‘𝐺)) |
| 39 | 38 | 3exp 1120 |
. . . . . 6
⊢ (𝐺 ∈ V → (𝐹(Walks‘𝐺)𝑃 → ((Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} ∈ (Edg‘𝐺)))) |
| 40 | 39 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 → ((Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} ∈ (Edg‘𝐺)))) |
| 41 | 1, 40 | mpcom 38 |
. . . 4
⊢ (𝐹(Walks‘𝐺)𝑃 → ((Fun (iEdg‘𝐺) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} ∈ (Edg‘𝐺))) |
| 42 | 41 | expd 415 |
. . 3
⊢ (𝐹(Walks‘𝐺)𝑃 → (Fun (iEdg‘𝐺) → (((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)) → {(𝑃‘0)} ∈ (Edg‘𝐺)))) |
| 43 | 42 | impcom 407 |
. 2
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝐹(Walks‘𝐺)𝑃) → (((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1)) → {(𝑃‘0)} ∈ (Edg‘𝐺))) |
| 44 | 43 | imp 406 |
1
⊢ (((Fun
(iEdg‘𝐺) ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} ∈ (Edg‘𝐺)) |