Step | Hyp | Ref
| Expression |
1 | | wwlksnextbij0.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | wwlknbp 28194 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) |
3 | | simp2 1136 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → 𝑁 ∈
ℕ0) |
4 | | wwlksnextbij0.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
5 | | wwlksnextbij0.d |
. . . 4
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} |
6 | | wwlksnextbij0.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} |
7 | | wwlksnextbij0.f |
. . . 4
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) |
8 | 1, 4, 5, 6, 7 | wwlksnextfun 28250 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |
9 | 2, 3, 8 | 3syl 18 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷⟶𝑅) |
10 | | preq2 4672 |
. . . . . 6
⊢ (𝑛 = 𝑟 → {(lastS‘𝑊), 𝑛} = {(lastS‘𝑊), 𝑟}) |
11 | 10 | eleq1d 2823 |
. . . . 5
⊢ (𝑛 = 𝑟 → ({(lastS‘𝑊), 𝑛} ∈ 𝐸 ↔ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) |
12 | 11, 6 | elrab2 3628 |
. . . 4
⊢ (𝑟 ∈ 𝑅 ↔ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) |
13 | 1, 4 | wwlksnext 28245 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸) → (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺)) |
14 | 13 | 3expb 1119 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺)) |
15 | | s1cl 14296 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ 𝑉 → 〈“𝑟”〉 ∈ Word 𝑉) |
16 | | pfxccat1 14404 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑟”〉 ∈ Word 𝑉) → ((𝑊 ++ 〈“𝑟”〉) prefix (♯‘𝑊)) = 𝑊) |
17 | 15, 16 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → ((𝑊 ++ 〈“𝑟”〉) prefix (♯‘𝑊)) = 𝑊) |
18 | 17 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word 𝑉 → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) prefix (♯‘𝑊)) = 𝑊)) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) prefix (♯‘𝑊)) = 𝑊)) |
20 | | oveq2 7277 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 + 1) = (♯‘𝑊) → ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = ((𝑊 ++ 〈“𝑟”〉) prefix (♯‘𝑊))) |
21 | 20 | eqcoms 2746 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑊) =
(𝑁 + 1) → ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = ((𝑊 ++ 〈“𝑟”〉) prefix (♯‘𝑊))) |
22 | 21 | eqeq1d 2740 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑊) =
(𝑁 + 1) → (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) prefix (♯‘𝑊)) = 𝑊)) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) prefix (♯‘𝑊)) = 𝑊)) |
24 | 19, 23 | sylibrd 258 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊)) |
25 | 24 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (𝑟 ∈ 𝑉 → ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊)) |
26 | 1, 4 | wwlknp 28195 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
27 | 25, 26 | syl11 33 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ 𝑉 → (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊)) |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸) → (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊)) |
29 | 28 | impcom 408 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊) |
30 | | lswccats1 14333 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → (lastS‘(𝑊 ++ 〈“𝑟”〉)) = 𝑟) |
31 | 30 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑟 ∈ 𝑉) → 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉))) |
32 | 31 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝑉 → (𝑟 ∈ 𝑉 → 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉)))) |
33 | 32 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word 𝑉) → (𝑟 ∈ 𝑉 → 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉)))) |
34 | 2, 33 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑟 ∈ 𝑉 → 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉)))) |
35 | 34 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉) → 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉))) |
36 | 35 | preq2d 4678 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉) → {(lastS‘𝑊), 𝑟} = {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))}) |
37 | 36 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉) → ({(lastS‘𝑊), 𝑟} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) |
38 | 37 | biimpd 228 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑉) → ({(lastS‘𝑊), 𝑟} ∈ 𝐸 → {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) |
39 | 38 | impr 455 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸) |
40 | 14, 29, 39 | jca32 516 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → ((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸))) |
41 | 33, 2 | syl11 33 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ 𝑉 → (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉)))) |
42 | 41 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸) → (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉)))) |
43 | 42 | impcom 408 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉))) |
44 | | ovexd 7304 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → (𝑊 ++ 〈“𝑟”〉) ∈ V) |
45 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺))) |
46 | | oveq1 7276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑑 prefix (𝑁 + 1)) = ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1))) |
47 | 46 | eqeq1d 2740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((𝑑 prefix (𝑁 + 1)) = 𝑊 ↔ ((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊)) |
48 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (lastS‘𝑑) = (lastS‘(𝑊 ++ 〈“𝑟”〉))) |
49 | 48 | preq2d 4678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → {(lastS‘𝑊), (lastS‘𝑑)} = {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))}) |
50 | 49 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ({(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) |
51 | 47, 50 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸) ↔ (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸))) |
52 | 45, 51 | anbi12d 631 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ↔ ((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)))) |
53 | 48 | eqeq2d 2749 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (𝑟 = (lastS‘𝑑) ↔ 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉)))) |
54 | 52, 53 | anbi12d 631 |
. . . . . . . . . . . . 13
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → (((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = (lastS‘𝑑)) ↔ (((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉))))) |
55 | 54 | bicomd 222 |
. . . . . . . . . . . 12
⊢ (𝑑 = (𝑊 ++ 〈“𝑟”〉) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉))) ↔ ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = (lastS‘𝑑)))) |
56 | 55 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) ∧ 𝑑 = (𝑊 ++ 〈“𝑟”〉)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉))) ↔ ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = (lastS‘𝑑)))) |
57 | 56 | biimpd 228 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) ∧ 𝑑 = (𝑊 ++ 〈“𝑟”〉)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉))) → ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = (lastS‘𝑑)))) |
58 | 44, 57 | spcimedv 3533 |
. . . . . . . . 9
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → ((((𝑊 ++ 〈“𝑟”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ (((𝑊 ++ 〈“𝑟”〉) prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘(𝑊 ++ 〈“𝑟”〉))} ∈ 𝐸)) ∧ 𝑟 = (lastS‘(𝑊 ++ 〈“𝑟”〉))) → ∃𝑑((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = (lastS‘𝑑)))) |
59 | 40, 43, 58 | mp2and 696 |
. . . . . . . 8
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = (lastS‘𝑑))) |
60 | | oveq1 7276 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑑 → (𝑤 prefix (𝑁 + 1)) = (𝑑 prefix (𝑁 + 1))) |
61 | 60 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑑 → ((𝑤 prefix (𝑁 + 1)) = 𝑊 ↔ (𝑑 prefix (𝑁 + 1)) = 𝑊)) |
62 | | fveq2 6768 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑑 → (lastS‘𝑤) = (lastS‘𝑑)) |
63 | 62 | preq2d 4678 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑑 → {(lastS‘𝑊), (lastS‘𝑤)} = {(lastS‘𝑊), (lastS‘𝑑)}) |
64 | 63 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑑 → ({(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) |
65 | 61, 64 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑑 → (((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸) ↔ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸))) |
66 | 65 | elrab 3625 |
. . . . . . . . . 10
⊢ (𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} ↔ (𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸))) |
67 | 66 | anbi1i 624 |
. . . . . . . . 9
⊢ ((𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} ∧ 𝑟 = (lastS‘𝑑)) ↔ ((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = (lastS‘𝑑))) |
68 | 67 | exbii 1850 |
. . . . . . . 8
⊢
(∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} ∧ 𝑟 = (lastS‘𝑑)) ↔ ∃𝑑((𝑑 ∈ ((𝑁 + 1) WWalksN 𝐺) ∧ ((𝑑 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑑)} ∈ 𝐸)) ∧ 𝑟 = (lastS‘𝑑))) |
69 | 59, 68 | sylibr 233 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} ∧ 𝑟 = (lastS‘𝑑))) |
70 | | df-rex 3070 |
. . . . . . 7
⊢
(∃𝑑 ∈
{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}𝑟 = (lastS‘𝑑) ↔ ∃𝑑(𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} ∧ 𝑟 = (lastS‘𝑑))) |
71 | 69, 70 | sylibr 233 |
. . . . . 6
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}𝑟 = (lastS‘𝑑)) |
72 | 1, 4, 5 | wwlksnextwrd 28249 |
. . . . . . . 8
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐷 = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}) |
73 | 72 | adantr 481 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → 𝐷 = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}) |
74 | 73 | rexeqdv 3348 |
. . . . . 6
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → (∃𝑑 ∈ 𝐷 𝑟 = (lastS‘𝑑) ↔ ∃𝑑 ∈ {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}𝑟 = (lastS‘𝑑))) |
75 | 71, 74 | mpbird 256 |
. . . . 5
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑 ∈ 𝐷 𝑟 = (lastS‘𝑑)) |
76 | | fveq2 6768 |
. . . . . . . 8
⊢ (𝑡 = 𝑑 → (lastS‘𝑡) = (lastS‘𝑑)) |
77 | | fvex 6781 |
. . . . . . . 8
⊢
(lastS‘𝑑)
∈ V |
78 | 76, 7, 77 | fvmpt 6869 |
. . . . . . 7
⊢ (𝑑 ∈ 𝐷 → (𝐹‘𝑑) = (lastS‘𝑑)) |
79 | 78 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑑 ∈ 𝐷 → (𝑟 = (𝐹‘𝑑) ↔ 𝑟 = (lastS‘𝑑))) |
80 | 79 | rexbiia 3179 |
. . . . 5
⊢
(∃𝑑 ∈
𝐷 𝑟 = (𝐹‘𝑑) ↔ ∃𝑑 ∈ 𝐷 𝑟 = (lastS‘𝑑)) |
81 | 75, 80 | sylibr 233 |
. . . 4
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑟 ∈ 𝑉 ∧ {(lastS‘𝑊), 𝑟} ∈ 𝐸)) → ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
82 | 12, 81 | sylan2b 594 |
. . 3
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑟 ∈ 𝑅) → ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
83 | 82 | ralrimiva 3103 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ∀𝑟 ∈ 𝑅 ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑)) |
84 | | dffo3 6972 |
. 2
⊢ (𝐹:𝐷–onto→𝑅 ↔ (𝐹:𝐷⟶𝑅 ∧ ∀𝑟 ∈ 𝑅 ∃𝑑 ∈ 𝐷 𝑟 = (𝐹‘𝑑))) |
85 | 9, 83, 84 | sylanbrc 583 |
1
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷–onto→𝑅) |