Proof of Theorem wwlksnextfun
| Step | Hyp | Ref
| Expression |
| 1 | | fveqeq2 6915 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((♯‘𝑤) = (𝑁 + 2) ↔ (♯‘𝑡) = (𝑁 + 2))) |
| 2 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (𝑤 prefix (𝑁 + 1)) = (𝑡 prefix (𝑁 + 1))) |
| 3 | 2 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((𝑤 prefix (𝑁 + 1)) = 𝑊 ↔ (𝑡 prefix (𝑁 + 1)) = 𝑊)) |
| 4 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → (lastS‘𝑤) = (lastS‘𝑡)) |
| 5 | 4 | preq2d 4740 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → {(lastS‘𝑊), (lastS‘𝑤)} = {(lastS‘𝑊), (lastS‘𝑡)}) |
| 6 | 5 | eleq1d 2826 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ({(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
| 7 | 1, 3, 6 | 3anbi123d 1438 |
. . . . 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 3695 |
. . . 4
⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) |
| 10 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 𝑡 ∈ Word 𝑉) |
| 11 | | nn0re 12535 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 12 | | 2re 12340 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
| 13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
| 14 | | nn0ge0 12551 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
| 15 | | 2pos 12369 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
| 16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 < 2) |
| 17 | 11, 13, 14, 16 | addgegt0d 11836 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
2)) |
| 18 | 17 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 0 < (𝑁 + 2)) |
| 19 | | breq2 5147 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑡) =
(𝑁 + 2) → (0 <
(♯‘𝑡) ↔ 0
< (𝑁 +
2))) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → (0 <
(♯‘𝑡) ↔ 0
< (𝑁 +
2))) |
| 21 | 18, 20 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 0 <
(♯‘𝑡)) |
| 22 | | hashgt0n0 14404 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word 𝑉 ∧ 0 < (♯‘𝑡)) → 𝑡 ≠ ∅) |
| 23 | 10, 21, 22 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → 𝑡 ≠ ∅) |
| 24 | 10, 23 | jca 511 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(♯‘𝑡) = (𝑁 + 2)) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
| 25 | 24 | expcom 413 |
. . . . . . . . . 10
⊢
((♯‘𝑡) =
(𝑁 + 2) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
| 26 | 25 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢
(((♯‘𝑡)
= (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
| 27 | 26 | expd 415 |
. . . . . . . 8
⊢
(((♯‘𝑡)
= (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸) → (𝑡 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)))) |
| 28 | 27 | impcom 407 |
. . . . . . 7
⊢ ((𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
| 29 | 28 | impcom 407 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
| 30 | | lswcl 14606 |
. . . . . 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 511 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((♯‘𝑡) = (𝑁 + 2) ∧ (𝑡 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸))) → ((lastS‘𝑡) ∈ 𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
| 34 | 9, 33 | sylan2b 594 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → ((lastS‘𝑡) ∈ 𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
| 35 | | preq2 4734 |
. . . . 5
⊢ (𝑛 = (lastS‘𝑡) → {(lastS‘𝑊), 𝑛} = {(lastS‘𝑊), (lastS‘𝑡)}) |
| 36 | 35 | eleq1d 2826 |
. . . 4
⊢ (𝑛 = (lastS‘𝑡) → ({(lastS‘𝑊), 𝑛} ∈ 𝐸 ↔ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
| 37 | | wwlksnextbij0.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} |
| 38 | 36, 37 | elrab2 3695 |
. . 3
⊢
((lastS‘𝑡)
∈ 𝑅 ↔
((lastS‘𝑡) ∈
𝑉 ∧ {(lastS‘𝑊), (lastS‘𝑡)} ∈ 𝐸)) |
| 39 | 34, 38 | sylibr 234 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → (lastS‘𝑡) ∈ 𝑅) |
| 40 | | wwlksnextbij0.f |
. 2
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) |
| 41 | 39, 40 | fmptd 7134 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |