Step | Hyp | Ref
| Expression |
1 | | wwlkextbij.d |
. . 3
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} |
2 | | wwlkextbij.r |
. . 3
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} |
3 | | wwlkextbij.f |
. . 3
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) |
4 | 1, 2, 3 | wwlkextfun 26257 |
. 2
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷⟶𝑅) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑡 = 𝑑 → ( lastS ‘𝑡) = ( lastS ‘𝑑)) |
6 | | fvex 6113 |
. . . . . . 7
⊢ ( lastS
‘𝑑) ∈
V |
7 | 5, 3, 6 | fvmpt 6191 |
. . . . . 6
⊢ (𝑑 ∈ 𝐷 → (𝐹‘𝑑) = ( lastS ‘𝑑)) |
8 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑡 = 𝑥 → ( lastS ‘𝑡) = ( lastS ‘𝑥)) |
9 | | fvex 6113 |
. . . . . . 7
⊢ ( lastS
‘𝑥) ∈
V |
10 | 8, 3, 9 | fvmpt 6191 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = ( lastS ‘𝑥)) |
11 | 7, 10 | eqeqan12d 2626 |
. . . . 5
⊢ ((𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝑑) = (𝐹‘𝑥) ↔ ( lastS ‘𝑑) = ( lastS ‘𝑥))) |
12 | 11 | adantl 481 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷)) → ((𝐹‘𝑑) = (𝐹‘𝑥) ↔ ( lastS ‘𝑑) = ( lastS ‘𝑥))) |
13 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑑 → (#‘𝑤) = (#‘𝑑)) |
14 | 13 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑤 = 𝑑 → ((#‘𝑤) = (𝑁 + 2) ↔ (#‘𝑑) = (𝑁 + 2))) |
15 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑤 = 𝑑 → (𝑤 substr 〈0, (𝑁 + 1)〉) = (𝑑 substr 〈0, (𝑁 + 1)〉)) |
16 | 15 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑤 = 𝑑 → ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
17 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑑 → ( lastS ‘𝑤) = ( lastS ‘𝑑)) |
18 | 17 | preq2d 4219 |
. . . . . . . . 9
⊢ (𝑤 = 𝑑 → {( lastS ‘𝑊), ( lastS ‘𝑤)} = {( lastS ‘𝑊), ( lastS ‘𝑑)}) |
19 | 18 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑤 = 𝑑 → ({( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) |
20 | 14, 16, 19 | 3anbi123d 1391 |
. . . . . . 7
⊢ (𝑤 = 𝑑 → (((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸))) |
21 | 20, 1 | elrab2 3333 |
. . . . . 6
⊢ (𝑑 ∈ 𝐷 ↔ (𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸))) |
22 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (#‘𝑤) = (#‘𝑥)) |
23 | 22 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ((#‘𝑤) = (𝑁 + 2) ↔ (#‘𝑥) = (𝑁 + 2))) |
24 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
25 | 24 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
26 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → ( lastS ‘𝑤) = ( lastS ‘𝑥)) |
27 | 26 | preq2d 4219 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → {( lastS ‘𝑊), ( lastS ‘𝑤)} = {( lastS ‘𝑊), ( lastS ‘𝑥)}) |
28 | 27 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ({( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) |
29 | 23, 25, 28 | 3anbi123d 1391 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) |
30 | 29, 1 | elrab2 3333 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) |
31 | | eqtr3 2631 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧
(#‘𝑥) = (𝑁 + 2)) → (#‘𝑑) = (#‘𝑥)) |
32 | 31 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑥) =
(𝑁 + 2) →
((#‘𝑑) = (𝑁 + 2) → (#‘𝑑) = (#‘𝑥))) |
33 | 32 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸) → ((#‘𝑑) = (𝑁 + 2) → (#‘𝑑) = (#‘𝑥))) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → ((#‘𝑑) = (𝑁 + 2) → (#‘𝑑) = (#‘𝑥))) |
35 | 34 | com12 32 |
. . . . . . . . . . . . 13
⊢
((#‘𝑑) =
(𝑁 + 2) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → (#‘𝑑) = (#‘𝑥))) |
36 | 35 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → (#‘𝑑) = (#‘𝑥))) |
37 | 36 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → (#‘𝑑) = (#‘𝑥))) |
38 | 37 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) → (#‘𝑑) = (#‘𝑥)) |
39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) →
(#‘𝑑) =
(#‘𝑥)) |
40 | 39 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑑 ∈ Word
𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥)) →
(#‘𝑑) =
(#‘𝑥)) |
41 | | simpr 476 |
. . . . . . . 8
⊢
(((((𝑑 ∈ Word
𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥)) → ( lastS
‘𝑑) = ( lastS
‘𝑥)) |
42 | | eqtr3 2631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊) → (𝑑 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
43 | | 1e2m1 11013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 = (2
− 1) |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ 1 = (2 − 1)) |
45 | 44 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) = (𝑁 + (2 −
1))) |
46 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
47 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℂ) |
48 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
49 | 46, 47, 48 | addsubassd 10291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 2) − 1)
= (𝑁 + (2 −
1))) |
50 | 45, 49 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) = ((𝑁 + 2) −
1)) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑑) = (𝑁 + 2)) → (𝑁 + 1) = ((𝑁 + 2) − 1)) |
52 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑑) =
(𝑁 + 2) →
((#‘𝑑) − 1) =
((𝑁 + 2) −
1)) |
53 | 52 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑑) =
(𝑁 + 2) → ((𝑁 + 1) = ((#‘𝑑) − 1) ↔ (𝑁 + 1) = ((𝑁 + 2) − 1))) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑑) = (𝑁 + 2)) → ((𝑁 + 1) = ((#‘𝑑) − 1) ↔ (𝑁 + 1) = ((𝑁 + 2) − 1))) |
55 | 51, 54 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑑) = (𝑁 + 2)) → (𝑁 + 1) = ((#‘𝑑) − 1)) |
56 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 + 1) = ((#‘𝑑) − 1) → 〈0,
(𝑁 + 1)〉 = 〈0,
((#‘𝑑) −
1)〉) |
57 | 56 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 + 1) = ((#‘𝑑) − 1) → (𝑑 substr 〈0, (𝑁 + 1)〉) = (𝑑 substr 〈0, ((#‘𝑑) −
1)〉)) |
58 | 56 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 + 1) = ((#‘𝑑) − 1) → (𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)) |
59 | 57, 58 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) = ((#‘𝑑) − 1) → ((𝑑 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉) ↔ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉))) |
60 | 55, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑑) = (𝑁 + 2)) → ((𝑑 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉) ↔ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉))) |
61 | 60 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑑) = (𝑁 + 2)) → ((𝑑 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉) → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉))) |
62 | 61 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ ((#‘𝑑) =
(𝑁 + 2) → ((𝑑 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉) → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
63 | 62 | com13 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉) →
((#‘𝑑) = (𝑁 + 2) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
64 | 42, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊) → ((#‘𝑑) = (𝑁 + 2) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
65 | 64 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 → ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 → ((#‘𝑑) = (𝑁 + 2) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉))))) |
66 | 65 | com23 84 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 → ((#‘𝑑) = (𝑁 + 2) → ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉))))) |
67 | 66 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊) → ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
68 | 67 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 → (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
69 | 68 | 3ad2ant2 1076 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸) → (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
70 | 69 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
71 | 70 | com12 32 |
. . . . . . . . . . . 12
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
72 | 71 | 3adant3 1074 |
. . . . . . . . . . 11
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
73 | 72 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → (𝑁 ∈ ℕ0 → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
74 | 73 | imp31 447 |
. . . . . . . . 9
⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)) |
75 | 74 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑑 ∈ Word
𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥)) → (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)) |
76 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) → 𝑑 ∈ Word 𝑉) |
77 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → 𝑥 ∈ Word 𝑉) |
78 | 76, 77 | anim12i 588 |
. . . . . . . . . . . 12
⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) → (𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉)) |
79 | 78 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) → (𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉)) |
80 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
81 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
83 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
84 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
2 |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 0 < 2) |
86 | 80, 82, 83, 85 | addgegt0d 10480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
2)) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧ 𝑁 ∈ ℕ0)
→ 0 < (𝑁 +
2)) |
88 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑑) =
(𝑁 + 2) → (0 <
(#‘𝑑) ↔ 0 <
(𝑁 + 2))) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧ 𝑁 ∈ ℕ0)
→ (0 < (#‘𝑑)
↔ 0 < (𝑁 +
2))) |
90 | 87, 89 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧ 𝑁 ∈ ℕ0)
→ 0 < (#‘𝑑)) |
91 | | hashgt0n0 13017 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ Word 𝑉 ∧ 0 < (#‘𝑑)) → 𝑑 ≠ ∅) |
92 | 90, 91 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ0)) → 𝑑 ≠ ∅) |
93 | 92 | exp32 629 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ Word 𝑉 → ((#‘𝑑) = (𝑁 + 2) → (𝑁 ∈ ℕ0 → 𝑑 ≠
∅))) |
94 | 93 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑑) =
(𝑁 + 2) → (𝑑 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → 𝑑 ≠
∅))) |
95 | 94 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑑) =
(𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸) → (𝑑 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → 𝑑 ≠
∅))) |
96 | 95 | impcom 445 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) → (𝑁 ∈ ℕ0 → 𝑑 ≠ ∅)) |
97 | 96 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) → (𝑁 ∈ ℕ0 → 𝑑 ≠ ∅)) |
98 | 97 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) → 𝑑 ≠ ∅) |
99 | 86 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ 𝑁 ∈ ℕ0)
→ 0 < (𝑁 +
2)) |
100 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑥) =
(𝑁 + 2) → (0 <
(#‘𝑥) ↔ 0 <
(𝑁 + 2))) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ 𝑁 ∈ ℕ0)
→ (0 < (#‘𝑥)
↔ 0 < (𝑁 +
2))) |
102 | 99, 101 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ 𝑁 ∈ ℕ0)
→ 0 < (#‘𝑥)) |
103 | | hashgt0n0 13017 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ Word 𝑉 ∧ 0 < (#‘𝑥)) → 𝑥 ≠ ∅) |
104 | 102, 103 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ0)) → 𝑥 ≠ ∅) |
105 | 104 | exp32 629 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Word 𝑉 → ((#‘𝑥) = (𝑁 + 2) → (𝑁 ∈ ℕ0 → 𝑥 ≠
∅))) |
106 | 105 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑥) =
(𝑁 + 2) → (𝑥 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → 𝑥 ≠
∅))) |
107 | 106 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑥) =
(𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸) → (𝑥 ∈ Word 𝑉 → (𝑁 ∈ ℕ0 → 𝑥 ≠
∅))) |
108 | 107 | impcom 445 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸)) → (𝑁 ∈ ℕ0 → 𝑥 ≠ ∅)) |
109 | 108 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) → (𝑁 ∈ ℕ0 → 𝑥 ≠ ∅)) |
110 | 109 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) → 𝑥 ≠ ∅) |
111 | 79, 98, 110 | jca32 556 |
. . . . . . . . . 10
⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) → ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅))) |
112 | 111 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑑 ∈ Word
𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥)) → ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅))) |
113 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → 𝑑 ∈ Word 𝑉) |
114 | 113 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → 𝑑 ∈ Word 𝑉) |
115 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → 𝑥 ∈ Word 𝑉) |
116 | 115 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ Word 𝑉) |
117 | | hashneq0 13016 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ Word 𝑉 → (0 < (#‘𝑑) ↔ 𝑑 ≠ ∅)) |
118 | 117 | biimprd 237 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ Word 𝑉 → (𝑑 ≠ ∅ → 0 < (#‘𝑑))) |
119 | 118 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → (𝑑 ≠ ∅ → 0 < (#‘𝑑))) |
120 | 119 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑑 ≠ ∅ → ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → 0 < (#‘𝑑))) |
121 | 120 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅) → ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → 0 < (#‘𝑑))) |
122 | 121 | impcom 445 |
. . . . . . . . . . 11
⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → 0 < (#‘𝑑)) |
123 | | 2swrd1eqwrdeq 13306 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ∧ 0 < (#‘𝑑)) → (𝑑 = 𝑥 ↔ ((#‘𝑑) = (#‘𝑥) ∧ ((𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) − 1)〉) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥))))) |
124 | 114, 116,
122, 123 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → (𝑑 = 𝑥 ↔ ((#‘𝑑) = (#‘𝑥) ∧ ((𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) − 1)〉) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥))))) |
125 | | ancom 465 |
. . . . . . . . . . . 12
⊢ (((𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) − 1)〉) ∧ (
lastS ‘𝑑) = ( lastS
‘𝑥)) ↔ (( lastS
‘𝑑) = ( lastS
‘𝑥) ∧ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉))) |
126 | 125 | anbi2i 726 |
. . . . . . . . . . 11
⊢
(((#‘𝑑) =
(#‘𝑥) ∧ ((𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) − 1)〉) ∧ (
lastS ‘𝑑) = ( lastS
‘𝑥))) ↔
((#‘𝑑) =
(#‘𝑥) ∧ (( lastS
‘𝑑) = ( lastS
‘𝑥) ∧ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
127 | | 3anass 1035 |
. . . . . . . . . . 11
⊢
(((#‘𝑑) =
(#‘𝑥) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥) ∧ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) − 1)〉)) ↔
((#‘𝑑) =
(#‘𝑥) ∧ (( lastS
‘𝑑) = ( lastS
‘𝑥) ∧ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉)))) |
128 | 126, 127 | bitr4i 266 |
. . . . . . . . . 10
⊢
(((#‘𝑑) =
(#‘𝑥) ∧ ((𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) − 1)〉) ∧ (
lastS ‘𝑑) = ( lastS
‘𝑥))) ↔
((#‘𝑑) =
(#‘𝑥) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥) ∧ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) −
1)〉))) |
129 | 124, 128 | syl6bb 275 |
. . . . . . . . 9
⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → (𝑑 = 𝑥 ↔ ((#‘𝑑) = (#‘𝑥) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) − 1)〉)))) |
130 | 112, 129 | syl 17 |
. . . . . . . 8
⊢
(((((𝑑 ∈ Word
𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥)) → (𝑑 = 𝑥 ↔ ((#‘𝑑) = (#‘𝑥) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr 〈0, ((#‘𝑑) − 1)〉) = (𝑥 substr 〈0, ((#‘𝑑) − 1)〉)))) |
131 | 40, 41, 75, 130 | mpbir3and 1238 |
. . . . . . 7
⊢
(((((𝑑 ∈ Word
𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) ∧ 𝑁 ∈ ℕ0) ∧ ( lastS
‘𝑑) = ( lastS
‘𝑥)) → 𝑑 = 𝑥) |
132 | 131 | exp31 628 |
. . . . . 6
⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ ran 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ ran 𝐸))) → (𝑁 ∈ ℕ0 → (( lastS
‘𝑑) = ( lastS
‘𝑥) → 𝑑 = 𝑥))) |
133 | 21, 30, 132 | syl2anb 495 |
. . . . 5
⊢ ((𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) → (𝑁 ∈ ℕ0 → (( lastS
‘𝑑) = ( lastS
‘𝑥) → 𝑑 = 𝑥))) |
134 | 133 | impcom 445 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷)) → (( lastS ‘𝑑) = ( lastS ‘𝑥) → 𝑑 = 𝑥)) |
135 | 12, 134 | sylbid 229 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷)) → ((𝐹‘𝑑) = (𝐹‘𝑥) → 𝑑 = 𝑥)) |
136 | 135 | ralrimivva 2954 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ∀𝑑 ∈
𝐷 ∀𝑥 ∈ 𝐷 ((𝐹‘𝑑) = (𝐹‘𝑥) → 𝑑 = 𝑥)) |
137 | | dff13 6416 |
. 2
⊢ (𝐹:𝐷–1-1→𝑅 ↔ (𝐹:𝐷⟶𝑅 ∧ ∀𝑑 ∈ 𝐷 ∀𝑥 ∈ 𝐷 ((𝐹‘𝑑) = (𝐹‘𝑥) → 𝑑 = 𝑥))) |
138 | 4, 136, 137 | sylanbrc 695 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝐷–1-1→𝑅) |