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