Step | Hyp | Ref
| Expression |
1 | | wwlksnextbij0.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | wwlknbp 26733 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) |
3 | | simp2 1062 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → 𝑁 ∈
ℕ0) |
4 | | wwlksnextbij0.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
5 | | wwlksnextbij0.d |
. . . 4
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} |
6 | | wwlksnextbij.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸} |
7 | | wwlksnextbij.f |
. . . 4
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) |
8 | 1, 4, 5, 6, 7 | wwlksnextfun 26793 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |
9 | 2, 3, 8 | 3syl 18 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷⟶𝑅) |
10 | | preq2 4269 |
. . . . . 6
⊢ (𝑛 = 𝑟 → {( lastS ‘𝑊), 𝑛} = {( lastS ‘𝑊), 𝑟}) |
11 | 10 | eleq1d 2686 |
. . . . 5
⊢ (𝑛 = 𝑟 → ({( lastS ‘𝑊), 𝑛} ∈ 𝐸 ↔ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) |
12 | 11, 6 | elrab2 3366 |
. . . 4
⊢ (𝑟 ∈ 𝑅 ↔ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) |
13 | 1, 4 | wwlksnext 26788 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸) → (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺)) |
14 | 13 | 3expb 1266 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺)) |
15 | | s1cl 13382 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ 𝑉 → 〈“𝑟”〉 ∈ Word 𝑉) |
16 | | swrdccat1 13457 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑟”〉 ∈ Word 𝑉) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊) |
17 | 15, 16 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊) |
18 | 17 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word 𝑉 → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊)) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊)) |
20 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) = (#‘𝑊) → 〈0, (𝑁 + 1)〉 = 〈0,
(#‘𝑊)〉) |
21 | 20 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑊) =
(𝑁 + 1) → 〈0,
(𝑁 + 1)〉 = 〈0,
(#‘𝑊)〉) |
22 | 21 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) =
(𝑁 + 1) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0,
(𝑁 + 1)〉) = ((𝑊 ++ 〈“𝑟”〉) substr 〈0,
(#‘𝑊)〉)) |
23 | 22 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) =
(𝑁 + 1) → (((𝑊 ++ 〈“𝑟”〉) substr 〈0,
(𝑁 + 1)〉) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊)) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (#‘𝑊)〉) = 𝑊)) |
25 | 19, 24 | sylibrd 249 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
26 | 25 | 3adant3 1081 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
27 | 1, 4 | wwlknp 26734 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
28 | 26, 27 | syl11 33 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ 𝑉 → (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
29 | 28 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸) → (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
30 | 29 | impcom 446 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊) |
31 | | lswccats1 13411 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → ( lastS ‘(𝑊 ++ 〈“𝑟”〉)) = 𝑟) |
32 | 31 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) |
33 | 32 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝑉 → (𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
34 | 33 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → (𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
35 | 2, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑟 ∈ 𝑉 → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
36 | 35 | imp 445 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) |
37 | 36 | preq2d 4275 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉) → {( lastS ‘𝑊), 𝑟} = {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))}) |
38 | 37 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉) → ({( lastS ‘𝑊), 𝑟} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) |
39 | 38 | biimpd 219 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉) → ({( lastS ‘𝑊), 𝑟} ∈ 𝐸 → {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) |
40 | 39 | impr 649 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸) |
41 | 14, 30, 40 | jca32 558 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → ((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸))) |
42 | 34, 2 | syl11 33 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ 𝑉 → (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
43 | 42 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸) → (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
44 | 43 | impcom 446 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) |
45 | | ovexd 6680 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → (𝑊 ++ 〈“𝑟”〉) ∈ V) |
46 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺))) |
47 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑑 substr 〈0, (𝑁 + 1)〉) = ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉)) |
48 | 47 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
49 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ( lastS ‘𝑑) = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) |
50 | 49 | preq2d 4275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → {( lastS ‘𝑊), ( lastS ‘𝑑)} = {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))}) |
51 | 50 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ({( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) |
52 | 48, 51 | anbi12d 747 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸) ↔ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸))) |
53 | 46, 52 | anbi12d 747 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ↔ ((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)))) |
54 | 49 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑟 = ( lastS ‘𝑑) ↔ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉)))) |
55 | 53, 54 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)) ↔ (((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))))) |
56 | 55 | bicomd 213 |
. . . . . . . . . . . 12
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) ↔ ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)))) |
57 | 56 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) ∧ 𝑑 = (𝑊 ++ 〈“𝑟”〉)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) ↔ ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)))) |
58 | 57 | biimpd 219 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) ∧ 𝑑 = (𝑊 ++ 〈“𝑟”〉)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) → ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)))) |
59 | 45, 58 | spcimedv 3292 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘(𝑊 ++ 〈“𝑟”〉))) → ∃𝑑((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑)))) |
60 | 41, 44, 59 | mp2and 715 |
. . . . . . . 8
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑))) |
61 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑑 → (𝑤 substr 〈0, (𝑁 + 1)〉) = (𝑑 substr 〈0, (𝑁 + 1)〉)) |
62 | 61 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑑 → ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
63 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑑 → ( lastS ‘𝑤) = ( lastS ‘𝑑)) |
64 | 63 | preq2d 4275 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑑 → {( lastS ‘𝑊), ( lastS ‘𝑤)} = {( lastS ‘𝑊), ( lastS ‘𝑑)}) |
65 | 64 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑑 → ({( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) |
66 | 62, 65 | anbi12d 747 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑑 → (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸) ↔ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸))) |
67 | 66 | elrab 3363 |
. . . . . . . . . 10
⊢ (𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} ↔ (𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸))) |
68 | 67 | anbi1i 731 |
. . . . . . . . 9
⊢ ((𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} ∧ 𝑟 = ( lastS ‘𝑑)) ↔ ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑))) |
69 | 68 | exbii 1774 |
. . . . . . . 8
⊢
(∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} ∧ 𝑟 = ( lastS ‘𝑑)) ↔ ∃𝑑((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = ( lastS ‘𝑑))) |
70 | 60, 69 | sylibr 224 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} ∧ 𝑟 = ( lastS ‘𝑑))) |
71 | | df-rex 2918 |
. . . . . . 7
⊢
(∃𝑑 ∈
{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}𝑟 = ( lastS ‘𝑑) ↔ ∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} ∧ 𝑟 = ( lastS ‘𝑑))) |
72 | 70, 71 | sylibr 224 |
. . . . . 6
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}𝑟 = ( lastS ‘𝑑)) |
73 | 1, 4, 5 | wwlksnextwrd 26792 |
. . . . . . . 8
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐷 = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}) |
74 | 73 | adantr 481 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → 𝐷 = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}) |
75 | 74 | rexeqdv 3145 |
. . . . . 6
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → (∃𝑑 ∈ 𝐷 𝑟 = ( lastS ‘𝑑) ↔ ∃𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}𝑟 = ( lastS ‘𝑑))) |
76 | 72, 75 | mpbird 247 |
. . . . 5
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑 ∈ 𝐷 𝑟 = ( lastS ‘𝑑)) |
77 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑡 = 𝑑 → ( lastS ‘𝑡) = ( lastS ‘𝑑)) |
78 | | fvex 6201 |
. . . . . . . 8
⊢ ( lastS
‘𝑑) ∈
V |
79 | 77, 7, 78 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑑 ∈ 𝐷 → (𝐹‘𝑑) = ( lastS ‘𝑑)) |
80 | 79 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑑 ∈ 𝐷 → (𝑟 = (𝐹‘𝑑) ↔ 𝑟 = ( lastS ‘𝑑))) |
81 | 80 | rexbiia 3040 |
. . . . 5
⊢
(∃𝑑 ∈
𝐷 𝑟 = (𝐹‘𝑑) ↔ ∃𝑑 ∈ 𝐷 𝑟 = ( lastS ‘𝑑)) |
82 | 76, 81 | sylibr 224 |
. . . 4
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {( lastS ‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
83 | 12, 82 | sylan2b 492 |
. . 3
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑅) → ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
84 | 83 | ralrimiva 2966 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ∀𝑟 ∈ 𝑅 ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
85 | | dffo3 6374 |
. 2
⊢ (𝐹:𝐷–onto→𝑅 ↔ (𝐹:𝐷⟶𝑅 ∧ ∀𝑟 ∈ 𝑅 ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑))) |
86 | 9, 84, 85 | sylanbrc 698 |
1
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷–onto→𝑅) |