| Step | Hyp | Ref
| Expression |
| 1 | | wlkp1.w |
. . . . . 6
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
| 2 | | wlkp1.i |
. . . . . . 7
⊢ 𝐼 = (iEdg‘𝐺) |
| 3 | 2 | wlkf 29632 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| 4 | | wrdf 14557 |
. . . . . . 7
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) |
| 5 | | wlkp1.n |
. . . . . . . . . 10
⊢ 𝑁 = (♯‘𝐹) |
| 6 | 5 | eqcomi 2746 |
. . . . . . . . 9
⊢
(♯‘𝐹) =
𝑁 |
| 7 | 6 | oveq2i 7442 |
. . . . . . . 8
⊢
(0..^(♯‘𝐹)) = (0..^𝑁) |
| 8 | 7 | feq2i 6728 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ↔ 𝐹:(0..^𝑁)⟶dom 𝐼) |
| 9 | 4, 8 | sylib 218 |
. . . . . 6
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^𝑁)⟶dom 𝐼) |
| 10 | 1, 3, 9 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶dom 𝐼) |
| 11 | 5 | fvexi 6920 |
. . . . . . 7
⊢ 𝑁 ∈ V |
| 12 | 11 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ V) |
| 13 | | wlkp1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 14 | | snidg 4660 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐵}) |
| 15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ {𝐵}) |
| 16 | | wlkp1.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) |
| 17 | | dmsnopg 6233 |
. . . . . . . 8
⊢ (𝐸 ∈ (Edg‘𝐺) → dom {〈𝐵, 𝐸〉} = {𝐵}) |
| 18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom {〈𝐵, 𝐸〉} = {𝐵}) |
| 19 | 15, 18 | eleqtrrd 2844 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ dom {〈𝐵, 𝐸〉}) |
| 20 | 12, 19 | fsnd 6891 |
. . . . 5
⊢ (𝜑 → {〈𝑁, 𝐵〉}:{𝑁}⟶dom {〈𝐵, 𝐸〉}) |
| 21 | | fzodisjsn 13737 |
. . . . . 6
⊢
((0..^𝑁) ∩
{𝑁}) =
∅ |
| 22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((0..^𝑁) ∩ {𝑁}) = ∅) |
| 23 | | fun 6770 |
. . . . 5
⊢ (((𝐹:(0..^𝑁)⟶dom 𝐼 ∧ {〈𝑁, 𝐵〉}:{𝑁}⟶dom {〈𝐵, 𝐸〉}) ∧ ((0..^𝑁) ∩ {𝑁}) = ∅) → (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})⟶(dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
| 24 | 10, 20, 22, 23 | syl21anc 838 |
. . . 4
⊢ (𝜑 → (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})⟶(dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
| 25 | | wlkp1.h |
. . . . . 6
⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) |
| 26 | 25 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉})) |
| 27 | | wlkp1.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
| 28 | | wlkp1.f |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐼) |
| 29 | | wlkp1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ Fin) |
| 30 | | wlkp1.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 31 | | wlkp1.d |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) |
| 32 | | wlkp1.x |
. . . . . . . 8
⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) |
| 33 | | wlkp1.u |
. . . . . . . 8
⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) |
| 34 | 27, 2, 28, 29, 13, 30, 31, 1, 5, 16, 32, 33, 25 | wlkp1lem2 29692 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐻) = (𝑁 + 1)) |
| 35 | 34 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^(𝑁 + 1))) |
| 36 | | wlkcl 29633 |
. . . . . . . 8
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
| 37 | | eleq1 2829 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
𝑁 →
((♯‘𝐹) ∈
ℕ0 ↔ 𝑁 ∈
ℕ0)) |
| 38 | 37 | eqcoms 2745 |
. . . . . . . . . 10
⊢ (𝑁 = (♯‘𝐹) → ((♯‘𝐹) ∈ ℕ0
↔ 𝑁 ∈
ℕ0)) |
| 39 | | elnn0uz 12923 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
| 40 | 39 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘0)) |
| 41 | 38, 40 | biimtrdi 253 |
. . . . . . . . 9
⊢ (𝑁 = (♯‘𝐹) → ((♯‘𝐹) ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘0))) |
| 42 | 5, 41 | ax-mp 5 |
. . . . . . . 8
⊢
((♯‘𝐹)
∈ ℕ0 → 𝑁 ∈
(ℤ≥‘0)) |
| 43 | 1, 36, 42 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
| 44 | | fzosplitsn 13814 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
| 45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
| 46 | 35, 45 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (0..^(♯‘𝐻)) = ((0..^𝑁) ∪ {𝑁})) |
| 47 | 33 | dmeqd 5916 |
. . . . . 6
⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ∪ {〈𝐵, 𝐸〉})) |
| 48 | | dmun 5921 |
. . . . . 6
⊢ dom
(𝐼 ∪ {〈𝐵, 𝐸〉}) = (dom 𝐼 ∪ dom {〈𝐵, 𝐸〉}) |
| 49 | 47, 48 | eqtrdi 2793 |
. . . . 5
⊢ (𝜑 → dom (iEdg‘𝑆) = (dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
| 50 | 26, 46, 49 | feq123d 6725 |
. . . 4
⊢ (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom (iEdg‘𝑆) ↔ (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})⟶(dom 𝐼 ∪ dom {〈𝐵, 𝐸〉}))) |
| 51 | 24, 50 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐻:(0..^(♯‘𝐻))⟶dom (iEdg‘𝑆)) |
| 52 | | iswrdb 14558 |
. . 3
⊢ (𝐻 ∈ Word dom
(iEdg‘𝑆) ↔ 𝐻:(0..^(♯‘𝐻))⟶dom (iEdg‘𝑆)) |
| 53 | 51, 52 | sylibr 234 |
. 2
⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆)) |
| 54 | 27 | wlkp 29634 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 55 | 1, 54 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 56 | 5 | oveq2i 7442 |
. . . . . . 7
⊢
(0...𝑁) =
(0...(♯‘𝐹)) |
| 57 | 56 | feq2i 6728 |
. . . . . 6
⊢ (𝑃:(0...𝑁)⟶𝑉 ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 58 | 55, 57 | sylibr 234 |
. . . . 5
⊢ (𝜑 → 𝑃:(0...𝑁)⟶𝑉) |
| 59 | | ovexd 7466 |
. . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈ V) |
| 60 | 59, 30 | fsnd 6891 |
. . . . 5
⊢ (𝜑 → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝑉) |
| 61 | | fzp1disj 13623 |
. . . . . 6
⊢
((0...𝑁) ∩
{(𝑁 + 1)}) =
∅ |
| 62 | 61 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅) |
| 63 | | fun 6770 |
. . . . 5
⊢ (((𝑃:(0...𝑁)⟶𝑉 ∧ {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝑉) ∧ ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅) → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉)) |
| 64 | 58, 60, 62, 63 | syl21anc 838 |
. . . 4
⊢ (𝜑 → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉)) |
| 65 | | fzsuc 13611 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)})) |
| 66 | 43, 65 | syl 17 |
. . . . 5
⊢ (𝜑 → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)})) |
| 67 | | unidm 4157 |
. . . . . . 7
⊢ (𝑉 ∪ 𝑉) = 𝑉 |
| 68 | 67 | eqcomi 2746 |
. . . . . 6
⊢ 𝑉 = (𝑉 ∪ 𝑉) |
| 69 | 68 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑉 = (𝑉 ∪ 𝑉)) |
| 70 | 66, 69 | feq23d 6731 |
. . . 4
⊢ (𝜑 → ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉 ↔ (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉))) |
| 71 | 64, 70 | mpbird 257 |
. . 3
⊢ (𝜑 → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉) |
| 72 | | wlkp1.q |
. . . . 5
⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) |
| 73 | 72 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})) |
| 74 | 34 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (0...(♯‘𝐻)) = (0...(𝑁 + 1))) |
| 75 | | wlkp1.s |
. . . 4
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
| 76 | 73, 74, 75 | feq123d 6725 |
. . 3
⊢ (𝜑 → (𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉)) |
| 77 | 71, 76 | mpbird 257 |
. 2
⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆)) |
| 78 | | wlkp1.l |
. . 3
⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) |
| 79 | 27, 2, 28, 29, 13, 30, 31, 1, 5, 16, 32, 33, 25, 72, 75, 78 | wlkp1lem8 29698 |
. 2
⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) |
| 80 | 27, 2, 28, 29, 13, 30, 31, 1, 5, 16, 32, 33, 25, 72, 75 | wlkp1lem4 29694 |
. . 3
⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
| 81 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
| 82 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
| 83 | 81, 82 | iswlk 29628 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))) |
| 84 | 80, 83 | syl 17 |
. 2
⊢ (𝜑 → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))) |
| 85 | 53, 77, 79, 84 | mpbir3and 1343 |
1
⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄) |