Proof of Theorem wwlkextfun
Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (#‘𝑤) = (#‘𝑡)) |
2 | 1 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((#‘𝑤) = (𝑁 + 2) ↔ (#‘𝑡) = (𝑁 + 2))) |
3 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → (𝑤 substr 〈0, (𝑁 + 1)〉) = (𝑡 substr 〈0, (𝑁 + 1)〉)) |
4 | 3 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
5 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → ( lastS ‘𝑤) = ( lastS ‘𝑡)) |
6 | 5 | preq2d 4219 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → {( lastS ‘𝑊), ( lastS ‘𝑤)} = {( lastS ‘𝑊), ( lastS ‘𝑡)}) |
7 | 6 | eleq1d 2672 |
. . . . . 6
⊢ (𝑤 = 𝑡 → ({( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)) |
8 | 2, 4, 7 | 3anbi123d 1391 |
. . . . 5
⊢ (𝑤 = 𝑡 → (((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸))) |
9 | | wwlkextbij.d |
. . . . 5
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} |
10 | 8, 9 | elrab2 3333 |
. . . 4
⊢ (𝑡 ∈ 𝐷 ↔ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸))) |
11 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → 𝑡 ∈ Word 𝑉) |
12 | | nn0re 11178 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
13 | | 2re 10967 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
14 | 13 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
15 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
16 | | 2pos 10989 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 0 < 2) |
18 | 12, 14, 15, 17 | addgegt0d 10480 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
2)) |
19 | 18 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → 0 < (𝑁 + 2)) |
20 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑡) =
(𝑁 + 2) → (0 <
(#‘𝑡) ↔ 0 <
(𝑁 + 2))) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → (0 <
(#‘𝑡) ↔ 0 <
(𝑁 + 2))) |
22 | 19, 21 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → 0 <
(#‘𝑡)) |
23 | | hashgt0n0 13017 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word 𝑉 ∧ 0 < (#‘𝑡)) → 𝑡 ≠ ∅) |
24 | 11, 22, 23 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → 𝑡 ≠ ∅) |
25 | 11, 24 | jca 553 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
(#‘𝑡) = (𝑁 + 2)) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
26 | 25 | expcom 450 |
. . . . . . . . . 10
⊢
((#‘𝑡) =
(𝑁 + 2) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
27 | 26 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢
(((#‘𝑡) =
(𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸) → ((𝑡 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
28 | 27 | expd 451 |
. . . . . . . 8
⊢
(((#‘𝑡) =
(𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸) → (𝑡 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)))) |
29 | 28 | impcom 445 |
. . . . . . 7
⊢ ((𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)) → (𝑁 ∈ ℕ0 → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅))) |
30 | 29 | impcom 445 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸))) → (𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅)) |
31 | | lswcl 13208 |
. . . . . 6
⊢ ((𝑡 ∈ Word 𝑉 ∧ 𝑡 ≠ ∅) → ( lastS ‘𝑡) ∈ 𝑉) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸))) → ( lastS ‘𝑡) ∈ 𝑉) |
33 | | simprr3 1104 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸))) → {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸) |
34 | 32, 33 | jca 553 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ Word 𝑉 ∧ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸))) → (( lastS ‘𝑡) ∈ 𝑉 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)) |
35 | 10, 34 | sylan2b 491 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → (( lastS ‘𝑡) ∈ 𝑉 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)) |
36 | | preq2 4213 |
. . . . 5
⊢ (𝑛 = ( lastS ‘𝑡) → {( lastS ‘𝑊), 𝑛} = {( lastS ‘𝑊), ( lastS ‘𝑡)}) |
37 | 36 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = ( lastS ‘𝑡) → ({( lastS ‘𝑊), 𝑛} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)) |
38 | | wwlkextbij.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} |
39 | 37, 38 | elrab2 3333 |
. . 3
⊢ (( lastS
‘𝑡) ∈ 𝑅 ↔ (( lastS ‘𝑡) ∈ 𝑉 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)) |
40 | 35, 39 | sylibr 223 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑡 ∈ 𝐷) → ( lastS ‘𝑡) ∈ 𝑅) |
41 | | wwlkextbij.f |
. 2
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) |
42 | 40, 41 | fmptd 6292 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |