Step | Hyp | Ref
| Expression |
1 | | 2nn0 11936 |
. . . 4
⊢ 2 ∈
ℕ0 |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ∈
ℕ0) |
3 | | lencl 13917 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
4 | 3 | adantr 485 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (♯‘𝑊) ∈
ℕ0) |
5 | | simpr 489 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ≤
(♯‘𝑊)) |
6 | | elfz2nn0 13032 |
. . 3
⊢ (2 ∈
(0...(♯‘𝑊))
↔ (2 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0 ∧ 2 ≤
(♯‘𝑊))) |
7 | 2, 4, 5, 6 | syl3anbrc 1341 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ∈
(0...(♯‘𝑊))) |
8 | | pfxlen 14077 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 2)) =
2) |
9 | | s2len 14283 |
. . . . . . 7
⊢
(♯‘〈“(𝑊‘0)(𝑊‘1)”〉) = 2 |
10 | 9 | eqcomi 2768 |
. . . . . 6
⊢ 2 =
(♯‘〈“(𝑊‘0)(𝑊‘1)”〉) |
11 | 10 | a1i 11 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → 2 =
(♯‘〈“(𝑊‘0)(𝑊‘1)”〉)) |
12 | | 2nn 11732 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
13 | | lbfzo0 13111 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^2) ↔ 2 ∈ ℕ) |
14 | 12, 13 | mpbir 234 |
. . . . . . . . 9
⊢ 0 ∈
(0..^2) |
15 | | pfxfv 14076 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊)) ∧ 0 ∈ (0..^2))
→ ((𝑊 prefix
2)‘0) = (𝑊‘0)) |
16 | 14, 15 | mp3an3 1448 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘0) = (𝑊‘0)) |
17 | 16 | adantr 485 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) = (𝑊‘0)) |
18 | | fvex 6664 |
. . . . . . . 8
⊢ (𝑊‘0) ∈
V |
19 | | s2fv0 14281 |
. . . . . . . 8
⊢ ((𝑊‘0) ∈ V →
(〈“(𝑊‘0)(𝑊‘1)”〉‘0) = (𝑊‘0)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢
(〈“(𝑊‘0)(𝑊‘1)”〉‘0) = (𝑊‘0) |
21 | 17, 20 | eqtr4di 2812 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘0)) |
22 | | 1nn0 11935 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
23 | | 1lt2 11830 |
. . . . . . . . . 10
⊢ 1 <
2 |
24 | | elfzo0 13112 |
. . . . . . . . . 10
⊢ (1 ∈
(0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1
< 2)) |
25 | 22, 12, 23, 24 | mpbir3an 1339 |
. . . . . . . . 9
⊢ 1 ∈
(0..^2) |
26 | | pfxfv 14076 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊)) ∧ 1 ∈ (0..^2))
→ ((𝑊 prefix
2)‘1) = (𝑊‘1)) |
27 | 25, 26 | mp3an3 1448 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘1) = (𝑊‘1)) |
28 | | fvex 6664 |
. . . . . . . . 9
⊢ (𝑊‘1) ∈
V |
29 | | s2fv1 14282 |
. . . . . . . . 9
⊢ ((𝑊‘1) ∈ V →
(〈“(𝑊‘0)(𝑊‘1)”〉‘1) = (𝑊‘1)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . 8
⊢
(〈“(𝑊‘0)(𝑊‘1)”〉‘1) = (𝑊‘1) |
31 | 27, 30 | eqtr4di 2812 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘1) = (〈“(𝑊‘0)(𝑊‘1)”〉‘1)) |
32 | 31 | adantr 485 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘1) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘1)) |
33 | | 0nn0 11934 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
34 | | fveq2 6651 |
. . . . . . . . 9
⊢ (𝑖 = 0 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘0)) |
35 | | fveq2 6651 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘0)) |
36 | 34, 35 | eqeq12d 2775 |
. . . . . . . 8
⊢ (𝑖 = 0 → (((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ ((𝑊 prefix 2)‘0) = (〈“(𝑊‘0)(𝑊‘1)”〉‘0))) |
37 | | fveq2 6651 |
. . . . . . . . 9
⊢ (𝑖 = 1 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘1)) |
38 | | fveq2 6651 |
. . . . . . . . 9
⊢ (𝑖 = 1 → (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘1)) |
39 | 37, 38 | eqeq12d 2775 |
. . . . . . . 8
⊢ (𝑖 = 1 → (((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ ((𝑊 prefix 2)‘1) = (〈“(𝑊‘0)(𝑊‘1)”〉‘1))) |
40 | 36, 39 | ralprg 4582 |
. . . . . . 7
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) →
(∀𝑖 ∈ {0, 1}
((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (〈“(𝑊‘0)(𝑊‘1)”〉‘0) ∧
((𝑊 prefix 2)‘1) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘1)))) |
41 | 33, 22, 40 | mp2an 692 |
. . . . . 6
⊢
(∀𝑖 ∈
{0, 1} ((𝑊 prefix
2)‘𝑖) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (〈“(𝑊‘0)(𝑊‘1)”〉‘0) ∧
((𝑊 prefix 2)‘1) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘1))) |
42 | 21, 32, 41 | sylanbrc 587 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) →
∀𝑖 ∈ {0, 1}
((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)) |
43 | | eqeq1 2763 |
. . . . . . 7
⊢
((♯‘(𝑊
prefix 2)) = 2 → ((♯‘(𝑊 prefix 2)) =
(♯‘〈“(𝑊‘0)(𝑊‘1)”〉) ↔ 2 =
(♯‘〈“(𝑊‘0)(𝑊‘1)”〉))) |
44 | | oveq2 7151 |
. . . . . . . . 9
⊢
((♯‘(𝑊
prefix 2)) = 2 → (0..^(♯‘(𝑊 prefix 2))) = (0..^2)) |
45 | | fzo0to2pr 13156 |
. . . . . . . . 9
⊢ (0..^2) =
{0, 1} |
46 | 44, 45 | eqtrdi 2810 |
. . . . . . . 8
⊢
((♯‘(𝑊
prefix 2)) = 2 → (0..^(♯‘(𝑊 prefix 2))) = {0, 1}) |
47 | 46 | raleqdv 3327 |
. . . . . . 7
⊢
((♯‘(𝑊
prefix 2)) = 2 → (∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖) ↔ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖))) |
48 | 43, 47 | anbi12d 634 |
. . . . . 6
⊢
((♯‘(𝑊
prefix 2)) = 2 → (((♯‘(𝑊 prefix 2)) =
(♯‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)) ↔ (2 =
(♯‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)))) |
49 | 48 | adantl 486 |
. . . . 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)”〉‘𝑖)))) |
50 | 11, 42, 49 | mpbir2and 713 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) →
((♯‘(𝑊 prefix
2)) = (♯‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖))) |
51 | 8, 50 | mpdan 687 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) →
((♯‘(𝑊 prefix
2)) = (♯‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖))) |
52 | | pfxcl 14071 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 2) ∈ Word 𝑉) |
53 | | s2cli 14274 |
. . . . 5
⊢
〈“(𝑊‘0)(𝑊‘1)”〉 ∈ Word
V |
54 | | eqwrd 13941 |
. . . . 5
⊢ (((𝑊 prefix 2) ∈ Word 𝑉 ∧ 〈“(𝑊‘0)(𝑊‘1)”〉 ∈ Word V) →
((𝑊 prefix 2) =
〈“(𝑊‘0)(𝑊‘1)”〉 ↔
((♯‘(𝑊 prefix
2)) = (♯‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)))) |
55 | 52, 53, 54 | sylancl 590 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉 ↔
((♯‘(𝑊 prefix
2)) = (♯‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)))) |
56 | 55 | adantr 485 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉 ↔
((♯‘(𝑊 prefix
2)) = (♯‘〈“(𝑊‘0)(𝑊‘1)”〉) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(〈“(𝑊‘0)(𝑊‘1)”〉‘𝑖)))) |
57 | 51, 56 | mpbird 260 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → (𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉) |
58 | 7, 57 | syldan 595 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (𝑊 prefix 2) = 〈“(𝑊‘0)(𝑊‘1)”〉) |