Step | Hyp | Ref
| Expression |
1 | | wlkp1.w |
. . . . . 6
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
2 | | wlkp1.i |
. . . . . . 7
⊢ 𝐼 = (iEdg‘𝐺) |
3 | 2 | wlkf 27981 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
4 | | wrdf 14222 |
. . . . . . 7
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) |
5 | | wlkp1.n |
. . . . . . . . . 10
⊢ 𝑁 = (♯‘𝐹) |
6 | 5 | eqcomi 2747 |
. . . . . . . . 9
⊢
(♯‘𝐹) =
𝑁 |
7 | 6 | oveq2i 7286 |
. . . . . . . 8
⊢
(0..^(♯‘𝐹)) = (0..^𝑁) |
8 | 7 | feq2i 6592 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ↔ 𝐹:(0..^𝑁)⟶dom 𝐼) |
9 | 4, 8 | sylib 217 |
. . . . . 6
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^𝑁)⟶dom 𝐼) |
10 | 1, 3, 9 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶dom 𝐼) |
11 | 5 | fvexi 6788 |
. . . . . . 7
⊢ 𝑁 ∈ V |
12 | 11 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ V) |
13 | | wlkp1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
14 | | snidg 4595 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐵}) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ {𝐵}) |
16 | | wlkp1.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) |
17 | | dmsnopg 6116 |
. . . . . . . 8
⊢ (𝐸 ∈ (Edg‘𝐺) → dom {〈𝐵, 𝐸〉} = {𝐵}) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom {〈𝐵, 𝐸〉} = {𝐵}) |
19 | 15, 18 | eleqtrrd 2842 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ dom {〈𝐵, 𝐸〉}) |
20 | 12, 19 | fsnd 6759 |
. . . . 5
⊢ (𝜑 → {〈𝑁, 𝐵〉}:{𝑁}⟶dom {〈𝐵, 𝐸〉}) |
21 | | fzodisjsn 13425 |
. . . . . 6
⊢
((0..^𝑁) ∩
{𝑁}) =
∅ |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((0..^𝑁) ∩ {𝑁}) = ∅) |
23 | | fun 6636 |
. . . . 5
⊢ (((𝐹:(0..^𝑁)⟶dom 𝐼 ∧ {〈𝑁, 𝐵〉}:{𝑁}⟶dom {〈𝐵, 𝐸〉}) ∧ ((0..^𝑁) ∩ {𝑁}) = ∅) → (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})⟶(dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
24 | 10, 20, 22, 23 | syl21anc 835 |
. . . 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 28042 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐻) = (𝑁 + 1)) |
35 | 34 | oveq2d 7291 |
. . . . . 6
⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^(𝑁 + 1))) |
36 | | wlkcl 27982 |
. . . . . . . 8
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
37 | | eleq1 2826 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
𝑁 →
((♯‘𝐹) ∈
ℕ0 ↔ 𝑁 ∈
ℕ0)) |
38 | 37 | eqcoms 2746 |
. . . . . . . . . 10
⊢ (𝑁 = (♯‘𝐹) → ((♯‘𝐹) ∈ ℕ0
↔ 𝑁 ∈
ℕ0)) |
39 | | elnn0uz 12623 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
40 | 39 | biimpi 215 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘0)) |
41 | 38, 40 | syl6bi 252 |
. . . . . . . . 9
⊢ (𝑁 = (♯‘𝐹) → ((♯‘𝐹) ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘0))) |
42 | 5, 41 | ax-mp 5 |
. . . . . . . 8
⊢
((♯‘𝐹)
∈ ℕ0 → 𝑁 ∈
(ℤ≥‘0)) |
43 | 1, 36, 42 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
44 | | fzosplitsn 13495 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
46 | 35, 45 | eqtrd 2778 |
. . . . 5
⊢ (𝜑 → (0..^(♯‘𝐻)) = ((0..^𝑁) ∪ {𝑁})) |
47 | 33 | dmeqd 5814 |
. . . . . 6
⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ∪ {〈𝐵, 𝐸〉})) |
48 | | dmun 5819 |
. . . . . 6
⊢ dom
(𝐼 ∪ {〈𝐵, 𝐸〉}) = (dom 𝐼 ∪ dom {〈𝐵, 𝐸〉}) |
49 | 47, 48 | eqtrdi 2794 |
. . . . 5
⊢ (𝜑 → dom (iEdg‘𝑆) = (dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
50 | 26, 46, 49 | feq123d 6589 |
. . . 4
⊢ (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom (iEdg‘𝑆) ↔ (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})⟶(dom 𝐼 ∪ dom {〈𝐵, 𝐸〉}))) |
51 | 24, 50 | mpbird 256 |
. . 3
⊢ (𝜑 → 𝐻:(0..^(♯‘𝐻))⟶dom (iEdg‘𝑆)) |
52 | | iswrdb 14223 |
. . 3
⊢ (𝐻 ∈ Word dom
(iEdg‘𝑆) ↔ 𝐻:(0..^(♯‘𝐻))⟶dom (iEdg‘𝑆)) |
53 | 51, 52 | sylibr 233 |
. 2
⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆)) |
54 | 27 | wlkp 27983 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
55 | 1, 54 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
56 | 5 | oveq2i 7286 |
. . . . . . 7
⊢
(0...𝑁) =
(0...(♯‘𝐹)) |
57 | 56 | feq2i 6592 |
. . . . . 6
⊢ (𝑃:(0...𝑁)⟶𝑉 ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉) |
58 | 55, 57 | sylibr 233 |
. . . . 5
⊢ (𝜑 → 𝑃:(0...𝑁)⟶𝑉) |
59 | | ovexd 7310 |
. . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈ V) |
60 | 59, 30 | fsnd 6759 |
. . . . 5
⊢ (𝜑 → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝑉) |
61 | | fzp1disj 13315 |
. . . . . 6
⊢
((0...𝑁) ∩
{(𝑁 + 1)}) =
∅ |
62 | 61 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅) |
63 | | fun 6636 |
. . . . 5
⊢ (((𝑃:(0...𝑁)⟶𝑉 ∧ {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝑉) ∧ ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅) → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉)) |
64 | 58, 60, 62, 63 | syl21anc 835 |
. . . 4
⊢ (𝜑 → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉)) |
65 | | fzsuc 13303 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)})) |
66 | 43, 65 | syl 17 |
. . . . 5
⊢ (𝜑 → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)})) |
67 | | unidm 4086 |
. . . . . . 7
⊢ (𝑉 ∪ 𝑉) = 𝑉 |
68 | 67 | eqcomi 2747 |
. . . . . 6
⊢ 𝑉 = (𝑉 ∪ 𝑉) |
69 | 68 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑉 = (𝑉 ∪ 𝑉)) |
70 | 66, 69 | feq23d 6595 |
. . . 4
⊢ (𝜑 → ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉 ↔ (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉))) |
71 | 64, 70 | mpbird 256 |
. . 3
⊢ (𝜑 → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉) |
72 | | wlkp1.q |
. . . . 5
⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) |
73 | 72 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})) |
74 | 34 | oveq2d 7291 |
. . . 4
⊢ (𝜑 → (0...(♯‘𝐻)) = (0...(𝑁 + 1))) |
75 | | wlkp1.s |
. . . 4
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
76 | 73, 74, 75 | feq123d 6589 |
. . 3
⊢ (𝜑 → (𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉)) |
77 | 71, 76 | mpbird 256 |
. 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 28048 |
. 2
⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) |
80 | 27, 2, 28, 29, 13, 30, 31, 1, 5, 16, 32, 33, 25, 72, 75 | wlkp1lem4 28044 |
. . 3
⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
81 | | eqid 2738 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
82 | | eqid 2738 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
83 | 81, 82 | iswlk 27977 |
. . 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 1341 |
1
⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄) |