Step | Hyp | Ref
| Expression |
1 | | wwlknprop 26214 |
. . 3
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉))) |
2 | | simprl 790 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → 𝑁 ∈
ℕ0) |
3 | | wwlkextbij.d |
. . . 4
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} |
4 | | wwlkextbij.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} |
5 | | wwlkextbij.f |
. . . 4
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) |
6 | 3, 4, 5 | wwlkextfun 26257 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |
7 | 1, 2, 6 | 3syl 18 |
. 2
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐹:𝐷⟶𝑅) |
8 | | preq2 4213 |
. . . . . 6
⊢ (𝑛 = 𝑟 → {( lastS ‘𝑊), 𝑛} = {( lastS ‘𝑊), 𝑟}) |
9 | 8 | eleq1d 2672 |
. . . . 5
⊢ (𝑛 = 𝑟 → ({( lastS ‘𝑊), 𝑛} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) |
10 | 9, 4 | elrab2 3333 |
. . . 4
⊢ (𝑟 ∈ 𝑅 ↔ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) |
11 | | wwlknext 26252 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸) → (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) |
12 | 11 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) |
13 | | wwlknimp 26215 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
14 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ 𝑉 → 〈“𝑟”〉 ∈ Word 𝑉) |
15 | | swrdccat1 13309 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑟”〉 ∈ Word 𝑉) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊) |
16 | 14, 15 | sylan2 490 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊) |
17 | 16 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝑉 → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊)) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊)) |
19 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 + 1) = (#‘𝑊) → 〈0, (𝑁 + 1)〉 = 〈0,
(#‘𝑊)〉) |
20 | 19 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) =
(𝑁 + 1) → 〈0,
(𝑁 + 1)〉 = 〈0,
(#‘𝑊)〉) |
21 | 20 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑊) =
(𝑁 + 1) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0,
(𝑁 + 1)〉) = ((𝑊 ++ 〈“𝑟”〉) substr 〈0,
(#‘𝑊)〉)) |
22 | 21 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) =
(𝑁 + 1) → (((𝑊 ++ 〈“𝑟”〉) substr 〈0,
(𝑁 + 1)〉) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊)) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊)) |
24 | 18, 23 | sylibrd 248 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
25 | 24 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
26 | 13, 25 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
27 | 26 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ 𝑉 → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
28 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
29 | 28 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊) |
30 | | lswccats1 13263 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → ( lastS ‘(𝑊 ++ 〈“𝑟”〉)) = 𝑟) |
31 | 30 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) |
32 | 31 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ Word 𝑉 → (𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
33 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → (𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉)) → (𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
35 | 1, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
36 | 35 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑟 ∈ 𝑉) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) |
37 | 36 | preq2d 4219 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑟 ∈ 𝑉) → {( lastS ‘𝑊), 𝑟} = {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))}) |
38 | 37 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑟 ∈ 𝑉) → ({( lastS ‘𝑊), 𝑟} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)) |
39 | 38 | biimpd 218 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑟 ∈ 𝑉) → ({( lastS ‘𝑊), 𝑟} ∈ ran 𝐸 → {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)) |
40 | 39 | impr 647 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸) |
41 | 12, 29, 40 | jca32 556 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → ((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸))) |
42 | 35 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ 𝑉 → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
43 | 42 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
44 | 43 | impcom 445 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) |
45 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑊 ++ 〈“𝑟”〉) ∈
V |
46 | 45 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → (𝑊 ++ 〈“𝑟”〉) ∈ V) |
47 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))) |
48 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑑 substr 〈0, (𝑁 + 1)〉) = ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉)) |
49 | 48 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
50 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ( lastS ‘𝑑) = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) |
51 | 50 | preq2d 4219 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → {( lastS ‘𝑊), ( lastS ‘𝑑)} = {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))}) |
52 | 51 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ({( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)) |
53 | 49, 52 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸) ↔ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸))) |
54 | 47, 53 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ↔ ((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)))) |
55 | 50 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑟 = ( lastS ‘𝑑) ↔ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
56 | 54, 55 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)) ↔ (((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))))) |
57 | 56 | bicomd 212 |
. . . . . . . . . . . 12
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) ↔ ((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)))) |
58 | 57 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) ∧ 𝑑 = (𝑊 ++ 〈“𝑟”〉)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) ↔ ((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)))) |
59 | 58 | biimpd 218 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) ∧ 𝑑 = (𝑊 ++ 〈“𝑟”〉)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) → ((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)))) |
60 | 46, 59 | spcimedv 3265 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) → ∃𝑑((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)))) |
61 | 41, 44, 60 | mp2and 711 |
. . . . . . . 8
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → ∃𝑑((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑))) |
62 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑑 → (𝑤 substr 〈0, (𝑁 + 1)〉) = (𝑑 substr 〈0, (𝑁 + 1)〉)) |
63 | 62 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑑 → ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
64 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑑 → ( lastS ‘𝑤) = ( lastS ‘𝑑)) |
65 | 64 | preq2d 4219 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑑 → {( lastS ‘𝑊), ( lastS ‘𝑤)} = {( lastS ‘𝑊), ( lastS ‘𝑑)}) |
66 | 65 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑑 → ({( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) |
67 | 63, 66 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑑 → (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸))) |
68 | 67 | elrab 3331 |
. . . . . . . . . 10
⊢ (𝑑 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} ↔ (𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸))) |
69 | 68 | anbi1i 727 |
. . . . . . . . 9
⊢ ((𝑑 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} ∧ 𝑟 = ( lastS ‘𝑑)) ↔ ((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑))) |
70 | 69 | exbii 1764 |
. . . . . . . 8
⊢
(∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} ∧ 𝑟 = ( lastS ‘𝑑)) ↔ ∃𝑑((𝑑 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑))) |
71 | 61, 70 | sylibr 223 |
. . . . . . 7
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → ∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} ∧ 𝑟 = ( lastS ‘𝑑))) |
72 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑑 ∈
{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}𝑟 = ( lastS ‘𝑑) ↔ ∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} ∧ 𝑟 = ( lastS ‘𝑑))) |
73 | 71, 72 | sylibr 223 |
. . . . . 6
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → ∃𝑑 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}𝑟 = ( lastS ‘𝑑)) |
74 | 3 | wwlkextwrd 26256 |
. . . . . . . 8
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
75 | 74 | adantr 480 |
. . . . . . 7
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
76 | 75 | rexeqdv 3122 |
. . . . . 6
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → (∃𝑑 ∈ 𝐷 𝑟 = ( lastS ‘𝑑) ↔ ∃𝑑 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}𝑟 = ( lastS ‘𝑑))) |
77 | 73, 76 | mpbird 246 |
. . . . 5
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → ∃𝑑 ∈ 𝐷 𝑟 = ( lastS ‘𝑑)) |
78 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑡 = 𝑑 → ( lastS ‘𝑡) = ( lastS ‘𝑑)) |
79 | | fvex 6113 |
. . . . . . . 8
⊢ ( lastS
‘𝑑) ∈
V |
80 | 78, 5, 79 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑑 ∈ 𝐷 → (𝐹‘𝑑) = ( lastS ‘𝑑)) |
81 | 80 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑑 ∈ 𝐷 → (𝑟 = (𝐹‘𝑑) ↔ 𝑟 = ( lastS ‘𝑑))) |
82 | 81 | rexbiia 3022 |
. . . . 5
⊢
(∃𝑑 ∈
𝐷 𝑟 = (𝐹‘𝑑) ↔ ∃𝑑 ∈ 𝐷 𝑟 = ( lastS ‘𝑑)) |
83 | 77, 82 | sylibr 223 |
. . . 4
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ ran 𝐸)) → ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
84 | 10, 83 | sylan2b 491 |
. . 3
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑟 ∈ 𝑅) → ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
85 | 84 | ralrimiva 2949 |
. 2
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ∀𝑟 ∈ 𝑅 ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
86 | | dffo3 6282 |
. 2
⊢ (𝐹:𝐷–onto→𝑅 ↔ (𝐹:𝐷⟶𝑅 ∧ ∀𝑟 ∈ 𝑅 ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑))) |
87 | 7, 85, 86 | sylanbrc 695 |
1
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐹:𝐷–onto→𝑅) |