| Step | Hyp | Ref
| Expression |
| 1 | | wlkv 29630 |
. . 3
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
| 2 | | eqid 2737 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 3 | | eqid 2737 |
. . . . . . . . 9
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 4 | 2, 3 | iswlk 29628 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))))) |
| 5 | | simpr1 1195 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph) ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → 𝐹 ∈ Word dom (iEdg‘𝐺)) |
| 6 | | simpr2 1196 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph) ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) |
| 7 | | df-ifp 1064 |
. . . . . . . . . . . . . . . . 17
⊢
(if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ↔ (((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}) ∨ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) |
| 8 | | dfsn2 4639 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {(𝑃‘𝑘)} = {(𝑃‘𝑘), (𝑃‘𝑘)} |
| 9 | | preq2 4734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) → {(𝑃‘𝑘), (𝑃‘𝑘)} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 10 | 8, 9 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) → {(𝑃‘𝑘)} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 11 | 10 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) → (((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)} ↔ ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 12 | 11 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 13 | 12 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}) → ((((𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 14 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph) → 𝐺 ∈
UPGraph) |
| 15 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → 𝐹 ∈ Word dom (iEdg‘𝐺)) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 17 | 3, 16 | upgredginwlk 29654 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom
(iEdg‘𝐺)) →
(𝑘 ∈
(0..^(♯‘𝐹))
→ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺))) |
| 18 | 14, 15, 17 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) → (𝑘 ∈ (0..^(♯‘𝐹)) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺))) |
| 19 | 18 | imp 406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) |
| 20 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) → 𝐺 ∈ UPGraph) |
| 21 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → 𝐺 ∈ UPGraph) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐹 ∈ Word
dom (iEdg‘𝐺) ∧
𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) → 𝐺 ∈ UPGraph) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐹 ∈ Word
dom (iEdg‘𝐺) ∧
𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) ∧ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → 𝐺 ∈ UPGraph) |
| 24 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐹 ∈ Word
dom (iEdg‘𝐺) ∧
𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) ∧ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) |
| 25 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐹 ∈ Word
dom (iEdg‘𝐺) ∧
𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) ∧ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) |
| 26 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1))) |
| 27 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) → (𝑃‘𝑘) ∈ V) |
| 28 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) → (𝑃‘(𝑘 + 1)) ∈ V) |
| 29 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) |
| 30 | 27, 28, 29 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) → ((𝑃‘𝑘) ∈ V ∧ (𝑃‘(𝑘 + 1)) ∈ V ∧ (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
| 31 | 26, 30 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
(𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) → ((𝑃‘𝑘) ∈ V ∧ (𝑃‘(𝑘 + 1)) ∈ V ∧ (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((¬
(𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ((𝑃‘𝑘) ∈ V ∧ (𝑃‘(𝑘 + 1)) ∈ V ∧ (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
| 33 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐹 ∈ Word
dom (iEdg‘𝐺) ∧
𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) ∧ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((𝑃‘𝑘) ∈ V ∧ (𝑃‘(𝑘 + 1)) ∈ V ∧ (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
| 34 | 2, 16 | upgredgpr 29159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ UPGraph ∧
((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) ∧ ((𝑃‘𝑘) ∈ V ∧ (𝑃‘(𝑘 + 1)) ∈ V ∧ (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = ((iEdg‘𝐺)‘(𝐹‘𝑘))) |
| 35 | 23, 24, 25, 33, 34 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐹 ∈ Word
dom (iEdg‘𝐺) ∧
𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) ∧ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = ((iEdg‘𝐺)‘(𝐹‘𝑘))) |
| 36 | 35 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐹 ∈ Word
dom (iEdg‘𝐺) ∧
𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺)) ∧ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 37 | 36 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((iEdg‘𝐺)‘(𝐹‘𝑘)) ∈ (Edg‘𝐺) → ((¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 38 | 19, 37 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
(𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ((((𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 40 | 13, 39 | jaoi 858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}) ∨ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((((𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 41 | 40 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}) ∨ (¬ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 42 | 7, 41 | biimtrid 242 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 43 | 42 | ralimdva 3167 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph)) → (∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 44 | 43 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph) → (∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 45 | 44 | com23 86 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))) → (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph) → ∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 46 | 45 | 3impia 1118 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → (((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph) → ∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 47 | 46 | impcom 407 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph) ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 48 | 5, 6, 47 | 3jca 1129 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ 𝐺 ∈ UPGraph) ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘))))) → (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 49 | 48 | exp31 419 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐺 ∈ UPGraph → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))) |
| 50 | 49 | com23 86 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑘)))) → (𝐺 ∈ UPGraph → (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))) |
| 51 | 4, 50 | sylbid 240 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))) |
| 52 | 51 | impd 410 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐺 ∈ UPGraph) → (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 53 | 52 | impcom 407 |
. . . . 5
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝐺 ∈ UPGraph) ∧ (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 54 | 2, 3 | isupwlk 48052 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(UPWalks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 55 | 54 | adantl 481 |
. . . . 5
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝐺 ∈ UPGraph) ∧ (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(UPWalks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 56 | 53, 55 | mpbird 257 |
. . . 4
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝐺 ∈ UPGraph) ∧ (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) → 𝐹(UPWalks‘𝐺)𝑃) |
| 57 | 56 | exp31 419 |
. . 3
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → 𝐹(UPWalks‘𝐺)𝑃))) |
| 58 | 1, 57 | mpid 44 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → 𝐹(UPWalks‘𝐺)𝑃)) |
| 59 | 58 | impcom 407 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → 𝐹(UPWalks‘𝐺)𝑃) |