Step | Hyp | Ref
| Expression |
1 | | 2nn0 12435 |
. . . 4
⊢ 2 ∈
ℕ0 |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ∈
ℕ0) |
3 | | lencl 14427 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
4 | 3 | adantr 482 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (♯‘𝑊) ∈
ℕ0) |
5 | | simpr 486 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ≤
(♯‘𝑊)) |
6 | | elfz2nn0 13538 |
. . 3
⊢ (2 ∈
(0...(♯‘𝑊))
↔ (2 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0 ∧ 2 ≤
(♯‘𝑊))) |
7 | 2, 4, 5, 6 | syl3anbrc 1344 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ∈
(0...(♯‘𝑊))) |
8 | | pfxlen 14577 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 2)) =
2) |
9 | | s2len 14784 |
. . . . . . 7
⊢
(♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) = 2 |
10 | 9 | eqcomi 2742 |
. . . . . 6
⊢ 2 =
(♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) |
11 | 10 | a1i 11 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → 2 =
(♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩)) |
12 | | 2nn 12231 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
13 | | lbfzo0 13618 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^2) ↔ 2 ∈ ℕ) |
14 | 12, 13 | mpbir 230 |
. . . . . . . . 9
⊢ 0 ∈
(0..^2) |
15 | | pfxfv 14576 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊)) ∧ 0 ∈ (0..^2))
→ ((𝑊 prefix
2)‘0) = (𝑊‘0)) |
16 | 14, 15 | mp3an3 1451 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘0) = (𝑊‘0)) |
17 | 16 | adantr 482 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) = (𝑊‘0)) |
18 | | fvex 6856 |
. . . . . . . 8
⊢ (𝑊‘0) ∈
V |
19 | | s2fv0 14782 |
. . . . . . . 8
⊢ ((𝑊‘0) ∈ V →
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) = (𝑊‘0)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) = (𝑊‘0) |
21 | 17, 20 | eqtr4di 2791 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) =
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘0)) |
22 | | 1nn0 12434 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
23 | | 1lt2 12329 |
. . . . . . . . . 10
⊢ 1 <
2 |
24 | | elfzo0 13619 |
. . . . . . . . . 10
⊢ (1 ∈
(0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1
< 2)) |
25 | 22, 12, 23, 24 | mpbir3an 1342 |
. . . . . . . . 9
⊢ 1 ∈
(0..^2) |
26 | | pfxfv 14576 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊)) ∧ 1 ∈ (0..^2))
→ ((𝑊 prefix
2)‘1) = (𝑊‘1)) |
27 | 25, 26 | mp3an3 1451 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘1) = (𝑊‘1)) |
28 | | fvex 6856 |
. . . . . . . . 9
⊢ (𝑊‘1) ∈
V |
29 | | s2fv1 14783 |
. . . . . . . . 9
⊢ ((𝑊‘1) ∈ V →
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘1) = (𝑊‘1)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . 8
⊢
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘1) = (𝑊‘1) |
31 | 27, 30 | eqtr4di 2791 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1)) |
32 | 31 | adantr 482 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘1) =
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘1)) |
33 | | 0nn0 12433 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
34 | | fveq2 6843 |
. . . . . . . . 9
⊢ (𝑖 = 0 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘0)) |
35 | | fveq2 6843 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0)) |
36 | 34, 35 | eqeq12d 2749 |
. . . . . . . 8
⊢ (𝑖 = 0 → (((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0))) |
37 | | fveq2 6843 |
. . . . . . . . 9
⊢ (𝑖 = 1 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘1)) |
38 | | fveq2 6843 |
. . . . . . . . 9
⊢ (𝑖 = 1 → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1)) |
39 | 37, 38 | eqeq12d 2749 |
. . . . . . . 8
⊢ (𝑖 = 1 → (((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))) |
40 | 36, 39 | ralprg 4656 |
. . . . . . 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 691 |
. . . . . 6
⊢
(∀𝑖 ∈
{0, 1} ((𝑊 prefix
2)‘𝑖) =
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) ∧
((𝑊 prefix 2)‘1) =
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))) |
42 | 21, 32, 41 | sylanbrc 584 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) →
∀𝑖 ∈ {0, 1}
((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)) |
43 | | eqeq1 2737 |
. . . . . . 7
⊢
((♯‘(𝑊
prefix 2)) = 2 → ((♯‘(𝑊 prefix 2)) =
(♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ↔ 2 =
(♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩))) |
44 | | oveq2 7366 |
. . . . . . . . 9
⊢
((♯‘(𝑊
prefix 2)) = 2 → (0..^(♯‘(𝑊 prefix 2))) = (0..^2)) |
45 | | fzo0to2pr 13663 |
. . . . . . . . 9
⊢ (0..^2) =
{0, 1} |
46 | 44, 45 | eqtrdi 2789 |
. . . . . . . 8
⊢
((♯‘(𝑊
prefix 2)) = 2 → (0..^(♯‘(𝑊 prefix 2))) = {0, 1}) |
47 | 46 | raleqdv 3312 |
. . . . . . 7
⊢
((♯‘(𝑊
prefix 2)) = 2 → (∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))) |
48 | 43, 47 | anbi12d 632 |
. . . . . 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 483 |
. . . . 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 712 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) →
((♯‘(𝑊 prefix
2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))) |
51 | 8, 50 | mpdan 686 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) →
((♯‘(𝑊 prefix
2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))) |
52 | | pfxcl 14571 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 2) ∈ Word 𝑉) |
53 | | s2cli 14775 |
. . . . 5
⊢
⟨“(𝑊‘0)(𝑊‘1)”⟩ ∈ Word
V |
54 | | eqwrd 14451 |
. . . . 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 587 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩ ↔
((♯‘(𝑊 prefix
2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)))) |
56 | 55 | adantr 482 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩ ↔
((♯‘(𝑊 prefix
2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈
(0..^(♯‘(𝑊
prefix 2)))((𝑊 prefix
2)‘𝑖) =
(⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)))) |
57 | 51, 56 | mpbird 257 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩) |
58 | 7, 57 | syldan 592 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩) |