Step | Hyp | Ref
| Expression |
1 | | 1wlkp1.w |
. . . . . 6
⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) |
2 | | 1wlkp1.i |
. . . . . . 7
⊢ 𝐼 = (iEdg‘𝐺) |
3 | 2 | 1wlkf 40819 |
. . . . . 6
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
4 | | wrdf 13165 |
. . . . . . 7
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) |
5 | | 1wlkp1.n |
. . . . . . . . . 10
⊢ 𝑁 = (#‘𝐹) |
6 | 5 | eqcomi 2619 |
. . . . . . . . 9
⊢
(#‘𝐹) = 𝑁 |
7 | 6 | oveq2i 6560 |
. . . . . . . 8
⊢
(0..^(#‘𝐹)) =
(0..^𝑁) |
8 | 7 | feq2i 5950 |
. . . . . . 7
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ↔ 𝐹:(0..^𝑁)⟶dom 𝐼) |
9 | 4, 8 | sylib 207 |
. . . . . 6
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^𝑁)⟶dom 𝐼) |
10 | 1, 3, 9 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶dom 𝐼) |
11 | | fvex 6113 |
. . . . . . . 8
⊢
(#‘𝐹) ∈
V |
12 | 5, 11 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑁 ∈ V |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ V) |
14 | | 1wlkp1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ V) |
15 | | snidg 4153 |
. . . . . . . 8
⊢ (𝐵 ∈ V → 𝐵 ∈ {𝐵}) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ {𝐵}) |
17 | | 1wlkp1.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) |
18 | | dmsnopg 5524 |
. . . . . . . 8
⊢ (𝐸 ∈ (Edg‘𝐺) → dom {〈𝐵, 𝐸〉} = {𝐵}) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom {〈𝐵, 𝐸〉} = {𝐵}) |
20 | 16, 19 | eleqtrrd 2691 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ dom {〈𝐵, 𝐸〉}) |
21 | 13, 20 | fsnd 6091 |
. . . . 5
⊢ (𝜑 → {〈𝑁, 𝐵〉}:{𝑁}⟶dom {〈𝐵, 𝐸〉}) |
22 | | fzodisjsn 12374 |
. . . . . 6
⊢
((0..^𝑁) ∩
{𝑁}) =
∅ |
23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((0..^𝑁) ∩ {𝑁}) = ∅) |
24 | | fun 5979 |
. . . . 5
⊢ (((𝐹:(0..^𝑁)⟶dom 𝐼 ∧ {〈𝑁, 𝐵〉}:{𝑁}⟶dom {〈𝐵, 𝐸〉}) ∧ ((0..^𝑁) ∩ {𝑁}) = ∅) → (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})⟶(dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
25 | 10, 21, 23, 24 | syl21anc 1317 |
. . . 4
⊢ (𝜑 → (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})⟶(dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
26 | | 1wlkp1.h |
. . . . . 6
⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) |
27 | 26 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉})) |
28 | | 1wlkp1.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
29 | | 1wlkp1.f |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐼) |
30 | | 1wlkp1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ Fin) |
31 | | 1wlkp1.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
32 | | 1wlkp1.d |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) |
33 | | 1wlkp1.x |
. . . . . . . 8
⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) |
34 | | 1wlkp1.u |
. . . . . . . 8
⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) |
35 | 28, 2, 29, 30, 14, 31, 32, 1, 5, 17, 33, 34, 26 | 1wlkp1lem2 40883 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐻) = (𝑁 + 1)) |
36 | 35 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (0..^(#‘𝐻)) = (0..^(𝑁 + 1))) |
37 | | 1wlkcl 40820 |
. . . . . . . 8
⊢ (𝐹(1Walks‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
38 | | eleq1 2676 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 𝑁 → ((#‘𝐹) ∈ ℕ0
↔ 𝑁 ∈
ℕ0)) |
39 | 38 | eqcoms 2618 |
. . . . . . . . . 10
⊢ (𝑁 = (#‘𝐹) → ((#‘𝐹) ∈ ℕ0 ↔ 𝑁 ∈
ℕ0)) |
40 | | elnn0uz 11601 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
41 | 40 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘0)) |
42 | 39, 41 | syl6bi 242 |
. . . . . . . . 9
⊢ (𝑁 = (#‘𝐹) → ((#‘𝐹) ∈ ℕ0 → 𝑁 ∈
(ℤ≥‘0))) |
43 | 5, 42 | ax-mp 5 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
ℕ0 → 𝑁 ∈
(ℤ≥‘0)) |
44 | 1, 37, 43 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
45 | | fzosplitsn 12442 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
46 | 44, 45 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
47 | 36, 46 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (0..^(#‘𝐻)) = ((0..^𝑁) ∪ {𝑁})) |
48 | 34 | dmeqd 5248 |
. . . . . 6
⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ∪ {〈𝐵, 𝐸〉})) |
49 | | dmun 5253 |
. . . . . 6
⊢ dom
(𝐼 ∪ {〈𝐵, 𝐸〉}) = (dom 𝐼 ∪ dom {〈𝐵, 𝐸〉}) |
50 | 48, 49 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → dom (iEdg‘𝑆) = (dom 𝐼 ∪ dom {〈𝐵, 𝐸〉})) |
51 | 27, 47, 50 | feq123d 5947 |
. . . 4
⊢ (𝜑 → (𝐻:(0..^(#‘𝐻))⟶dom (iEdg‘𝑆) ↔ (𝐹 ∪ {〈𝑁, 𝐵〉}):((0..^𝑁) ∪ {𝑁})⟶(dom 𝐼 ∪ dom {〈𝐵, 𝐸〉}))) |
52 | 25, 51 | mpbird 246 |
. . 3
⊢ (𝜑 → 𝐻:(0..^(#‘𝐻))⟶dom (iEdg‘𝑆)) |
53 | | iswrdb 13166 |
. . 3
⊢ (𝐻 ∈ Word dom
(iEdg‘𝑆) ↔ 𝐻:(0..^(#‘𝐻))⟶dom (iEdg‘𝑆)) |
54 | 52, 53 | sylibr 223 |
. 2
⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆)) |
55 | 28 | 1wlkp 40821 |
. . . . . . 7
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉) |
56 | 1, 55 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉) |
57 | 5 | oveq2i 6560 |
. . . . . . 7
⊢
(0...𝑁) =
(0...(#‘𝐹)) |
58 | 57 | feq2i 5950 |
. . . . . 6
⊢ (𝑃:(0...𝑁)⟶𝑉 ↔ 𝑃:(0...(#‘𝐹))⟶𝑉) |
59 | 56, 58 | sylibr 223 |
. . . . 5
⊢ (𝜑 → 𝑃:(0...𝑁)⟶𝑉) |
60 | | ovex 6577 |
. . . . . . 7
⊢ (𝑁 + 1) ∈ V |
61 | 60 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈ V) |
62 | 61, 31 | fsnd 6091 |
. . . . 5
⊢ (𝜑 → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝑉) |
63 | | fzp1disj 12269 |
. . . . . 6
⊢
((0...𝑁) ∩
{(𝑁 + 1)}) =
∅ |
64 | 63 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅) |
65 | | fun 5979 |
. . . . 5
⊢ (((𝑃:(0...𝑁)⟶𝑉 ∧ {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝑉) ∧ ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅) → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉)) |
66 | 59, 62, 64, 65 | syl21anc 1317 |
. . . 4
⊢ (𝜑 → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉)) |
67 | | fzsuc 12258 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)})) |
68 | 44, 67 | syl 17 |
. . . . 5
⊢ (𝜑 → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)})) |
69 | | unidm 3718 |
. . . . . . 7
⊢ (𝑉 ∪ 𝑉) = 𝑉 |
70 | 69 | eqcomi 2619 |
. . . . . 6
⊢ 𝑉 = (𝑉 ∪ 𝑉) |
71 | 70 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑉 = (𝑉 ∪ 𝑉)) |
72 | 68, 71 | feq23d 5953 |
. . . 4
⊢ (𝜑 → ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉 ↔ (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):((0...𝑁) ∪ {(𝑁 + 1)})⟶(𝑉 ∪ 𝑉))) |
73 | 66, 72 | mpbird 246 |
. . 3
⊢ (𝜑 → (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉) |
74 | | 1wlkp1.q |
. . . . 5
⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) |
75 | 74 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})) |
76 | 35 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (0...(#‘𝐻)) = (0...(𝑁 + 1))) |
77 | | 1wlkp1.s |
. . . 4
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
78 | 75, 76, 77 | feq123d 5947 |
. . 3
⊢ (𝜑 → (𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}):(0...(𝑁 + 1))⟶𝑉)) |
79 | 73, 78 | mpbird 246 |
. 2
⊢ (𝜑 → 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆)) |
80 | | 1wlkp1.l |
. . 3
⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) |
81 | 28, 2, 29, 30, 14, 31, 32, 1, 5, 17, 33, 34, 26, 74, 77, 80 | 1wlkp1lem8 40889 |
. 2
⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) |
82 | 28, 2, 29, 30, 14, 31, 32, 1, 5, 17, 33, 34, 26, 74, 77 | 1wlkp1lem4 40885 |
. . 3
⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
83 | | eqid 2610 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
84 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
85 | 83, 84 | is1wlk 40813 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(1Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑘 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))) |
86 | 82, 85 | syl 17 |
. 2
⊢ (𝜑 → (𝐻(1Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑘 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))) |
87 | 54, 79, 81, 86 | mpbir3and 1238 |
1
⊢ (𝜑 → 𝐻(1Walks‘𝑆)𝑄) |