Proof of Theorem wwlksnextfun
Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (#‘𝑤) = (#‘𝑡)) |
2 | 1 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((#‘𝑤) = (𝑁 + 2) ↔ (#‘𝑡) = (𝑁 + 2))) |
3 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (𝑤 substr 〈0, (𝑁 + 1)〉) = (𝑡 substr 〈0, (𝑁 + 1)〉)) |
4 | 3 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
5 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → ( lastS ‘𝑤) = ( lastS ‘𝑡)) |
6 | 5 | preq2d 4275 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → {( lastS ‘𝑊), ( lastS ‘𝑤)} = {( lastS ‘𝑊), ( lastS ‘𝑡)}) |
7 | 6 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ({( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)) |
8 | 2, 4, 7 | 3anbi123d 1399 |
. . . . 5
⊢ (𝑤 = 𝑡 → (((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸) ↔ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸))) |
9 | | wwlksnextbij0.d |
. . . . 5
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} |
10 | 8, 9 | elrab2 3366 |
. . . 4
⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸))) |
11 | | simpll 790 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → 𝑡 ∈ Word 𝑉) |
12 | | nn0re 11301 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
13 | | 2re 11090 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
14 | 13 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
15 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
16 | | 2pos 11112 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 < 2) |
18 | 12, 14, 15, 17 | addgegt0d 10601 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
2)) |
19 | 18 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → 0 < (𝑁 + 2)) |
20 | | breq2 4657 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑡) =
(𝑁 + 2) → (0 <
(#‘𝑡) ↔ 0 <
(𝑁 + 2))) |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → (0 <
(#‘𝑡) ↔ 0 <
(𝑁 + 2))) |
22 | 19, 21 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → 0 <
(#‘𝑡)) |
23 | | hashgt0n0 13156 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word 𝑉 ∧ 0 < (#‘𝑡)) → 𝑡 ≠ ∅) |
24 | 11, 22, 23 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → 𝑡 ≠ ∅) |
25 | 11, 24 | jca 554 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
26 | 25 | expcom 451 |
. . . . . . . . . 10
⊢
((#‘𝑡) =
(𝑁 + 2) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
27 | 26 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢
(((#‘𝑡) =
(𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
28 | 27 | expd 452 |
. . . . . . . 8
⊢
(((#‘𝑡) =
(𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸) → (𝑡 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)))) |
29 | 28 | impcom 446 |
. . . . . . 7
⊢ ((𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)) → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
30 | 29 | impcom 446 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸))) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
31 | | lswcl 13355 |
. . . . . 6
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅) → ( lastS ‘𝑡) ∈ 𝑉) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸))) → ( lastS ‘𝑡) ∈ 𝑉) |
33 | | simprr3 1111 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸))) → {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸) |
34 | 32, 33 | jca 554 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸))) → (( lastS ‘𝑡) ∈ 𝑉 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)) |
35 | 10, 34 | sylan2b 492 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → (( lastS ‘𝑡) ∈ 𝑉 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)) |
36 | | preq2 4269 |
. . . . 5
⊢ (𝑛 = ( lastS ‘𝑡) → {( lastS ‘𝑊), 𝑛} = {( lastS ‘𝑊), ( lastS ‘𝑡)}) |
37 | 36 | eleq1d 2686 |
. . . 4
⊢ (𝑛 = ( lastS ‘𝑡) → ({( lastS ‘𝑊), 𝑛} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)) |
38 | | wwlksnextbij.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸} |
39 | 37, 38 | elrab2 3366 |
. . 3
⊢ (( lastS
‘𝑡) ∈ 𝑅 ↔ (( lastS ‘𝑡) ∈ 𝑉 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)) |
40 | 35, 39 | sylibr 224 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → ( lastS ‘𝑡) ∈ 𝑅) |
41 | | wwlksnextbij.f |
. 2
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) |
42 | 40, 41 | fmptd 6385 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |