Proof of Theorem pfxeq
Step | Hyp | Ref
| Expression |
1 | | pfxcl 41386 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝑀) ∈ Word 𝑉) |
2 | | pfxcl 41386 |
. . . . 5
⊢ (𝑈 ∈ Word 𝑉 → (𝑈 prefix 𝑁) ∈ Word 𝑉) |
3 | 1, 2 | anim12i 590 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → ((𝑊 prefix 𝑀) ∈ Word 𝑉 ∧ (𝑈 prefix 𝑁) ∈ Word 𝑉)) |
4 | 3 | 3ad2ant1 1082 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 prefix 𝑀) ∈ Word 𝑉 ∧ (𝑈 prefix 𝑁) ∈ Word 𝑉)) |
5 | | eqwrd 13346 |
. . 3
⊢ (((𝑊 prefix 𝑀) ∈ Word 𝑉 ∧ (𝑈 prefix 𝑁) ∈ Word 𝑉) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ ((#‘(𝑊 prefix 𝑀)) = (#‘(𝑈 prefix 𝑁)) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)))) |
6 | 4, 5 | syl 17 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ ((#‘(𝑊 prefix 𝑀)) = (#‘(𝑈 prefix 𝑁)) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)))) |
7 | | simpl 473 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉) |
8 | 7 | 3ad2ant1 1082 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑊 ∈ Word 𝑉) |
9 | | simpl 473 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑀 ∈
ℕ0) |
10 | 9 | 3ad2ant2 1083 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑀 ∈
ℕ0) |
11 | | lencl 13324 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (#‘𝑊) ∈
ℕ0) |
13 | 12 | 3ad2ant1 1082 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘𝑊) ∈
ℕ0) |
14 | | simpl 473 |
. . . . . . 7
⊢ ((𝑀 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)) → 𝑀 ≤ (#‘𝑊)) |
15 | 14 | 3ad2ant3 1084 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑀 ≤ (#‘𝑊)) |
16 | | elfz2nn0 12431 |
. . . . . 6
⊢ (𝑀 ∈ (0...(#‘𝑊)) ↔ (𝑀 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑀
≤ (#‘𝑊))) |
17 | 10, 13, 15, 16 | syl3anbrc 1246 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑀 ∈ (0...(#‘𝑊))) |
18 | | pfxlen 41391 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → (#‘(𝑊 prefix 𝑀)) = 𝑀) |
19 | 8, 17, 18 | syl2anc 693 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘(𝑊 prefix 𝑀)) = 𝑀) |
20 | | simpr 477 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → 𝑈 ∈ Word 𝑉) |
21 | 20 | 3ad2ant1 1082 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑈 ∈ Word 𝑉) |
22 | | simpr 477 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
23 | 22 | 3ad2ant2 1083 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑁 ∈
ℕ0) |
24 | | lencl 13324 |
. . . . . . . 8
⊢ (𝑈 ∈ Word 𝑉 → (#‘𝑈) ∈
ℕ0) |
25 | 24 | adantl 482 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (#‘𝑈) ∈
ℕ0) |
26 | 25 | 3ad2ant1 1082 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘𝑈) ∈
ℕ0) |
27 | | simpr 477 |
. . . . . . 7
⊢ ((𝑀 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)) → 𝑁 ≤ (#‘𝑈)) |
28 | 27 | 3ad2ant3 1084 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑁 ≤ (#‘𝑈)) |
29 | | elfz2nn0 12431 |
. . . . . 6
⊢ (𝑁 ∈ (0...(#‘𝑈)) ↔ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑈))) |
30 | 23, 26, 28, 29 | syl3anbrc 1246 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → 𝑁 ∈ (0...(#‘𝑈))) |
31 | | pfxlen 41391 |
. . . . 5
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈))) → (#‘(𝑈 prefix 𝑁)) = 𝑁) |
32 | 21, 30, 31 | syl2anc 693 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘(𝑈 prefix 𝑁)) = 𝑁) |
33 | 19, 32 | eqeq12d 2637 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((#‘(𝑊 prefix 𝑀)) = (#‘(𝑈 prefix 𝑁)) ↔ 𝑀 = 𝑁)) |
34 | 33 | anbi1d 741 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (((#‘(𝑊 prefix 𝑀)) = (#‘(𝑈 prefix 𝑁)) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)))) |
35 | 8 | adantr 481 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → 𝑊 ∈ Word 𝑉) |
36 | 17 | adantr 481 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → 𝑀 ∈ (0...(#‘𝑊))) |
37 | 35, 36, 18 | syl2anc 693 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (#‘(𝑊 prefix 𝑀)) = 𝑀) |
38 | 37 | oveq2d 6666 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (0..^(#‘(𝑊 prefix 𝑀))) = (0..^𝑀)) |
39 | 38 | raleqdv 3144 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^(#‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖))) |
40 | 35 | adantr 481 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ Word 𝑉) |
41 | 36 | adantr 481 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ (0...(#‘𝑊))) |
42 | | simpr 477 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀)) |
43 | | pfxfv 41399 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊)) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑊 prefix 𝑀)‘𝑖) = (𝑊‘𝑖)) |
44 | 40, 41, 42, 43 | syl3anc 1326 |
. . . . . 6
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑊 prefix 𝑀)‘𝑖) = (𝑊‘𝑖)) |
45 | 21 | ad2antrr 762 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑈 ∈ Word 𝑉) |
46 | 30 | ad2antrr 762 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑁 ∈ (0...(#‘𝑈))) |
47 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁)) |
48 | 47 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝑀 = 𝑁 → (𝑖 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑁))) |
49 | 48 | adantl 482 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (𝑖 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑁))) |
50 | 49 | biimpa 501 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑁)) |
51 | | pfxfv 41399 |
. . . . . . 7
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑈 prefix 𝑁)‘𝑖) = (𝑈‘𝑖)) |
52 | 45, 46, 50, 51 | syl3anc 1326 |
. . . . . 6
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑈 prefix 𝑁)‘𝑖) = (𝑈‘𝑖)) |
53 | 44, 52 | eqeq12d 2637 |
. . . . 5
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ (𝑊‘𝑖) = (𝑈‘𝑖))) |
54 | 53 | ralbidva 2985 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^𝑀)((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))) |
55 | 39, 54 | bitrd 268 |
. . 3
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^(#‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))) |
56 | 55 | pm5.32da 673 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |
57 | 6, 34, 56 | 3bitrd 294 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |