Proof of Theorem wwlksnextfun
Step | Hyp | Ref
| Expression |
1 | | fveqeq2 6683 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((♯‘𝑤) = (𝑁 + 2) ↔ (♯‘𝑡) = (𝑁 + 2))) |
2 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (𝑤 prefix (𝑁 + 1)) = (𝑡 prefix (𝑁 + 1))) |
3 | 2 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((𝑤 prefix (𝑁 + 1)) = 𝑊 ↔ (𝑡 prefix (𝑁 + 1)) = 𝑊)) |
4 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → (lastS‘𝑤) = (lastS‘𝑡)) |
5 | 4 | preq2d 4631 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → {(lastS‘𝑊), (lastS‘𝑤)} = {(lastS‘𝑊), (lastS‘𝑡)}) |
6 | 5 | eleq1d 2817 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ({(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
7 | 1, 3, 6 | 3anbi123d 1437 |
. . . . 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 3591 |
. . . 4
⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) |
10 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 𝑡 ∈ Word 𝑉) |
11 | | nn0re 11985 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
12 | | 2re 11790 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
14 | | nn0ge0 12001 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
15 | | 2pos 11819 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 < 2) |
17 | 11, 13, 14, 16 | addgegt0d 11291 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
2)) |
18 | 17 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 0 < (𝑁 + 2)) |
19 | | breq2 5034 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑡) =
(𝑁 + 2) → (0 <
(♯‘𝑡) ↔ 0
< (𝑁 +
2))) |
20 | 19 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → (0 <
(♯‘𝑡) ↔ 0
< (𝑁 +
2))) |
21 | 18, 20 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 0 <
(♯‘𝑡)) |
22 | | hashgt0n0 13818 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word 𝑉 ∧ 0 < (♯‘𝑡)) → 𝑡 ≠ ∅) |
23 | 10, 21, 22 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 𝑡 ≠ ∅) |
24 | 10, 23 | jca 515 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
25 | 24 | expcom 417 |
. . . . . . . . . 10
⊢
((♯‘𝑡) =
(𝑁 + 2) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
26 | 25 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢
(((♯‘𝑡)
= (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
27 | 26 | expd 419 |
. . . . . . . 8
⊢
(((♯‘𝑡)
= (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸) → (𝑡 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)))) |
28 | 27 | impcom 411 |
. . . . . . 7
⊢ ((𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
29 | 28 | impcom 411 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
30 | | lswcl 14009 |
. . . . . 6
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅) → (lastS‘𝑡) ∈ 𝑉) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → (lastS‘𝑡) ∈ 𝑉) |
32 | | simprr3 1224 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸) |
33 | 31, 32 | jca 515 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → ((lastS‘𝑡) ∈ 𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
34 | 9, 33 | sylan2b 597 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → ((lastS‘𝑡) ∈ 𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
35 | | preq2 4625 |
. . . . 5
⊢ (𝑛 = (lastS‘𝑡) → {(lastS‘𝑊), 𝑛} = {(lastS‘𝑊), (lastS‘𝑡)}) |
36 | 35 | eleq1d 2817 |
. . . 4
⊢ (𝑛 = (lastS‘𝑡) → ({(lastS‘𝑊), 𝑛} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
37 | | wwlksnextbij0.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} |
38 | 36, 37 | elrab2 3591 |
. . 3
⊢
((lastS‘𝑡)
∈ 𝑅 ↔
((lastS‘𝑡) ∈
𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
39 | 34, 38 | sylibr 237 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → (lastS‘𝑡) ∈ 𝑅) |
40 | | wwlksnextbij0.f |
. 2
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) |
41 | 39, 40 | fmptd 6888 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |