Step | Hyp | Ref
| Expression |
1 | | 2nn0 11309 |
. . . 4
⊢ 2 ∈
ℕ0 |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → 2 ∈
ℕ0) |
3 | | lencl 13324 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
4 | 3 | adantr 481 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → (#‘𝑊) ∈
ℕ0) |
5 | | simpr 477 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → 2 ≤ (#‘𝑊)) |
6 | | elfz2nn0 12431 |
. . 3
⊢ (2 ∈
(0...(#‘𝑊)) ↔ (2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧ 2 ≤
(#‘𝑊))) |
7 | 2, 4, 5, 6 | syl3anbrc 1246 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → 2 ∈ (0...(#‘𝑊))) |
8 | | pfxlen 41391 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (#‘(𝑊 prefix 2)) =
2) |
9 | | s2len 13634 |
. . . . . . 7
⊢
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) = 2 |
10 | 9 | eqcomi 2631 |
. . . . . 6
⊢ 2 =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) |
11 | 10 | a1i 11 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → 2 =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉)) |
12 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → 𝑊 ∈ Word 𝑉) |
13 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → 2 ∈
(0...(#‘𝑊))) |
14 | | 2nn 11185 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
15 | | lbfzo0 12507 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^2) ↔ 2 ∈ ℕ) |
16 | 14, 15 | mpbir 221 |
. . . . . . . . . . 11
⊢ 0 ∈
(0..^2) |
17 | 16 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → 0 ∈
(0..^2)) |
18 | 12, 13, 17 | 3jca 1242 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊)) ∧ 0 ∈
(0..^2))) |
19 | 18 | adantr 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → (𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊)) ∧ 0 ∈
(0..^2))) |
20 | | pfxfv 41399 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0..^2))
→ ((𝑊 prefix
2)‘0) = (𝑊‘0)) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) = (𝑊‘0)) |
22 | | fvex 6201 |
. . . . . . . 8
⊢ (𝑊‘0) ∈
V |
23 | | s2fv0 13632 |
. . . . . . . 8
⊢ ((𝑊‘0) ∈ V →
(〈“(𝑊‘0)(𝑊‘1)”〉‘0) = (𝑊‘0)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
⊢
(〈“(𝑊‘0)(𝑊‘1)”〉‘0) = (𝑊‘0) |
25 | 21, 24 | syl6eqr 2674 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘0)) |
26 | | 1nn0 11308 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
27 | | 1lt2 11194 |
. . . . . . . . . 10
⊢ 1 <
2 |
28 | | elfzo0 12508 |
. . . . . . . . . 10
⊢ (1 ∈
(0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1
< 2)) |
29 | 26, 14, 27, 28 | mpbir3an 1244 |
. . . . . . . . 9
⊢ 1 ∈
(0..^2) |
30 | | pfxfv 41399 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊)) ∧ 1 ∈ (0..^2))
→ ((𝑊 prefix
2)‘1) = (𝑊‘1)) |
31 | 29, 30 | mp3an3 1413 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 2)‘1) = (𝑊‘1)) |
32 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝑊‘1) ∈
V |
33 | | s2fv1 13633 |
. . . . . . . . 9
⊢ ((𝑊‘1) ∈ V →
(〈“(𝑊‘0)(𝑊‘1)”〉‘1) = (𝑊‘1)) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . 8
⊢
(〈“(𝑊‘0)(𝑊‘1)”〉‘1) = (𝑊‘1) |
35 | 31, 34 | syl6eqr 2674 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 2)‘1) = (〈“(𝑊‘0)(𝑊‘1)”〉‘1)) |
36 | 35 | adantr 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘1) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘1)) |
37 | | 0nn0 11307 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
38 | 37, 26 | pm3.2i 471 |
. . . . . . . 8
⊢ (0 ∈
ℕ0 ∧ 1 ∈ ℕ0) |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → (0
∈ ℕ0 ∧ 1 ∈
ℕ0)) |
40 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑖 = 0 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘0)) |
41 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘0)) |
42 | 40, 41 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑖 = 0 → (((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ ((𝑊 prefix 2)‘0) = (〈“(𝑊‘0)(𝑊‘1)”〉‘0))) |
43 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑖 = 1 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘1)) |
44 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑖 = 1 → (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘1)) |
45 | 43, 44 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑖 = 1 → (((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ ((𝑊 prefix 2)‘1) = (〈“(𝑊‘0)(𝑊‘1)”〉‘1))) |
46 | 42, 45 | ralprg 4234 |
. . . . . . 7
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) →
(∀𝑖 ∈ {0, 1}
((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (〈“(𝑊‘0)(𝑊‘1)”〉‘0) ∧
((𝑊 prefix 2)‘1) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘1)))) |
47 | 39, 46 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) →
(∀𝑖 ∈ {0, 1}
((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (〈“(𝑊‘0)(𝑊‘1)”〉‘0) ∧
((𝑊 prefix 2)‘1) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘1)))) |
48 | 25, 36, 47 | mpbir2and 957 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) →
∀𝑖 ∈ {0, 1}
((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)) |
49 | | eqeq1 2626 |
. . . . . . 7
⊢
((#‘(𝑊 prefix
2)) = 2 → ((#‘(𝑊
prefix 2)) = (#‘〈“(𝑊‘0)(𝑊‘1)”〉) ↔ 2 =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉))) |
50 | | oveq2 6658 |
. . . . . . . . 9
⊢
((#‘(𝑊 prefix
2)) = 2 → (0..^(#‘(𝑊 prefix 2))) = (0..^2)) |
51 | | fzo0to2pr 12553 |
. . . . . . . . 9
⊢ (0..^2) =
{0, 1} |
52 | 50, 51 | syl6eq 2672 |
. . . . . . . 8
⊢
((#‘(𝑊 prefix
2)) = 2 → (0..^(#‘(𝑊 prefix 2))) = {0, 1}) |
53 | 52 | raleqdv 3144 |
. . . . . . 7
⊢
((#‘(𝑊 prefix
2)) = 2 → (∀𝑖
∈ (0..^(#‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖))) |
54 | 49, 53 | anbi12d 747 |
. . . . . 6
⊢
((#‘(𝑊 prefix
2)) = 2 → (((#‘(𝑊 prefix 2)) = (#‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)) ↔ (2 =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)))) |
55 | 54 | adantl 482 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) →
(((#‘(𝑊 prefix 2)) =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)) ↔ (2 =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)))) |
56 | 11, 48, 55 | mpbir2and 957 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) →
((#‘(𝑊 prefix 2)) =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖))) |
57 | 8, 56 | mpdan 702 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ((#‘(𝑊 prefix 2)) =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖))) |
58 | | pfxcl 41386 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 2) ∈ Word 𝑉) |
59 | 58 | adantr 481 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊 prefix 2) ∈ Word 𝑉) |
60 | | simp2 1062 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧ 2 ≤
(#‘𝑊)) →
(#‘𝑊) ∈
ℕ0) |
61 | | 1red 10055 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ0 → 1 ∈ ℝ) |
62 | | 2re 11090 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ0 → 2 ∈ ℝ) |
64 | | nn0re 11301 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℝ) |
65 | 61, 63, 64 | 3jca 1242 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) ∈
ℕ0 → (1 ∈ ℝ ∧ 2 ∈ ℝ ∧
(#‘𝑊) ∈
ℝ)) |
66 | | ltleletr 10130 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((1 < 2 ∧ 2
≤ (#‘𝑊)) → 1
≤ (#‘𝑊))) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢
((#‘𝑊) ∈
ℕ0 → ((1 < 2 ∧ 2 ≤ (#‘𝑊)) → 1 ≤ (#‘𝑊))) |
68 | 27, 67 | mpani 712 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
ℕ0 → (2 ≤ (#‘𝑊) → 1 ≤ (#‘𝑊))) |
69 | 68 | imp 445 |
. . . . . . . . . . 11
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 2 ≤ (#‘𝑊)) → 1 ≤ (#‘𝑊)) |
70 | 69 | 3adant1 1079 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧ 2 ≤
(#‘𝑊)) → 1 ≤
(#‘𝑊)) |
71 | 60, 70 | jca 554 |
. . . . . . . . 9
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧ 2 ≤
(#‘𝑊)) →
((#‘𝑊) ∈
ℕ0 ∧ 1 ≤ (#‘𝑊))) |
72 | | elnnnn0c 11338 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ ↔ ((#‘𝑊)
∈ ℕ0 ∧ 1 ≤ (#‘𝑊))) |
73 | 71, 72 | sylibr 224 |
. . . . . . . 8
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧ 2 ≤
(#‘𝑊)) →
(#‘𝑊) ∈
ℕ) |
74 | 6, 73 | sylbi 207 |
. . . . . . 7
⊢ (2 ∈
(0...(#‘𝑊)) →
(#‘𝑊) ∈
ℕ) |
75 | | lbfzo0 12507 |
. . . . . . 7
⊢ (0 ∈
(0..^(#‘𝑊)) ↔
(#‘𝑊) ∈
ℕ) |
76 | 74, 75 | sylibr 224 |
. . . . . 6
⊢ (2 ∈
(0...(#‘𝑊)) → 0
∈ (0..^(#‘𝑊))) |
77 | | wrdsymbcl 13318 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0..^(#‘𝑊))) → (𝑊‘0) ∈ 𝑉) |
78 | 76, 77 | sylan2 491 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊‘0) ∈ 𝑉) |
79 | 26 | a1i 11 |
. . . . . . 7
⊢ (2 ∈
(0...(#‘𝑊)) → 1
∈ ℕ0) |
80 | 65 | adantl 482 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0) → (1
∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ)) |
81 | | ltletr 10129 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((1 < 2 ∧ 2
≤ (#‘𝑊)) → 1
< (#‘𝑊))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0) → ((1
< 2 ∧ 2 ≤ (#‘𝑊)) → 1 < (#‘𝑊))) |
83 | 27, 82 | mpani 712 |
. . . . . . . . 9
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0) → (2 ≤
(#‘𝑊) → 1 <
(#‘𝑊))) |
84 | 83 | 3impia 1261 |
. . . . . . . 8
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧ 2 ≤
(#‘𝑊)) → 1 <
(#‘𝑊)) |
85 | 6, 84 | sylbi 207 |
. . . . . . 7
⊢ (2 ∈
(0...(#‘𝑊)) → 1
< (#‘𝑊)) |
86 | | elfzo0 12508 |
. . . . . . 7
⊢ (1 ∈
(0..^(#‘𝑊)) ↔ (1
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 1 < (#‘𝑊))) |
87 | 79, 74, 85, 86 | syl3anbrc 1246 |
. . . . . 6
⊢ (2 ∈
(0...(#‘𝑊)) → 1
∈ (0..^(#‘𝑊))) |
88 | | wrdsymbcl 13318 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ∈ (0..^(#‘𝑊))) → (𝑊‘1) ∈ 𝑉) |
89 | 87, 88 | sylan2 491 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊‘1) ∈ 𝑉) |
90 | 78, 89 | s2cld 13616 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → 〈“(𝑊‘0)(𝑊‘1)”〉 ∈ Word 𝑉) |
91 | | eqwrd 13346 |
. . . 4
⊢ (((𝑊 prefix 2) ∈ Word 𝑉 ∧ 〈“(𝑊‘0)(𝑊‘1)”〉 ∈ Word 𝑉) → ((𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉 ↔
((#‘(𝑊 prefix 2)) =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)))) |
92 | 59, 90, 91 | syl2anc 693 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉 ↔
((#‘(𝑊 prefix 2)) =
(#‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)))) |
93 | 57, 92 | mpbird 247 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉) |
94 | 7, 93 | syldan 487 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → (𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉) |