Proof of Theorem wwlksnextfun
Step | Hyp | Ref
| Expression |
1 | | fveqeq2 6783 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((♯‘𝑤) = (𝑁 + 2) ↔ (♯‘𝑡) = (𝑁 + 2))) |
2 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (𝑤 prefix (𝑁 + 1)) = (𝑡 prefix (𝑁 + 1))) |
3 | 2 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((𝑤 prefix (𝑁 + 1)) = 𝑊 ↔ (𝑡 prefix (𝑁 + 1)) = 𝑊)) |
4 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → (lastS‘𝑤) = (lastS‘𝑡)) |
5 | 4 | preq2d 4676 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → {(lastS‘𝑊), (lastS‘𝑤)} = {(lastS‘𝑊), (lastS‘𝑡)}) |
6 | 5 | eleq1d 2823 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ({(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
7 | 1, 3, 6 | 3anbi123d 1435 |
. . . . 5
⊢ (𝑤 = 𝑡 → (((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸) ↔ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) |
8 | | wwlksnextbij0.d |
. . . . 5
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} |
9 | 7, 8 | elrab2 3627 |
. . . 4
⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) |
10 | | simpll 764 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 𝑡 ∈ Word 𝑉) |
11 | | nn0re 12242 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
12 | | 2re 12047 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
14 | | nn0ge0 12258 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
15 | | 2pos 12076 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 < 2) |
17 | 11, 13, 14, 16 | addgegt0d 11548 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
2)) |
18 | 17 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 0 < (𝑁 + 2)) |
19 | | breq2 5078 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑡) =
(𝑁 + 2) → (0 <
(♯‘𝑡) ↔ 0
< (𝑁 +
2))) |
20 | 19 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → (0 <
(♯‘𝑡) ↔ 0
< (𝑁 +
2))) |
21 | 18, 20 | mpbird 256 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 0 <
(♯‘𝑡)) |
22 | | hashgt0n0 14080 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word 𝑉 ∧ 0 < (♯‘𝑡)) → 𝑡 ≠ ∅) |
23 | 10, 21, 22 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 𝑡 ≠ ∅) |
24 | 10, 23 | jca 512 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
25 | 24 | expcom 414 |
. . . . . . . . . 10
⊢
((♯‘𝑡) =
(𝑁 + 2) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
26 | 25 | 3ad2ant1 1132 |
. . . . . . . . 9
⊢
(((♯‘𝑡)
= (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
27 | 26 | expd 416 |
. . . . . . . 8
⊢
(((♯‘𝑡)
= (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸) → (𝑡 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)))) |
28 | 27 | impcom 408 |
. . . . . . 7
⊢ ((𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
29 | 28 | impcom 408 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
30 | | lswcl 14271 |
. . . . . 6
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅) → (lastS‘𝑡) ∈ 𝑉) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → (lastS‘𝑡) ∈ 𝑉) |
32 | | simprr3 1222 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸) |
33 | 31, 32 | jca 512 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → ((lastS‘𝑡) ∈ 𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
34 | 9, 33 | sylan2b 594 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → ((lastS‘𝑡) ∈ 𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
35 | | preq2 4670 |
. . . . 5
⊢ (𝑛 = (lastS‘𝑡) → {(lastS‘𝑊), 𝑛} = {(lastS‘𝑊), (lastS‘𝑡)}) |
36 | 35 | eleq1d 2823 |
. . . 4
⊢ (𝑛 = (lastS‘𝑡) → ({(lastS‘𝑊), 𝑛} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
37 | | wwlksnextbij0.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} |
38 | 36, 37 | elrab2 3627 |
. . 3
⊢
((lastS‘𝑡)
∈ 𝑅 ↔
((lastS‘𝑡) ∈
𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
39 | 34, 38 | sylibr 233 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → (lastS‘𝑡) ∈ 𝑅) |
40 | | wwlksnextbij0.f |
. 2
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) |
41 | 39, 40 | fmptd 6988 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |