Proof of Theorem pfxeq
Step | Hyp | Ref
| Expression |
1 | | pfxcl 13756 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝑀) ∈ Word 𝑉) |
2 | | pfxcl 13756 |
. . . . 5
⊢ (𝑈 ∈ Word 𝑉 → (𝑈 prefix 𝑁) ∈ Word 𝑉) |
3 | 1, 2 | anim12i 608 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → ((𝑊 prefix 𝑀) ∈ Word 𝑉 ∧ (𝑈 prefix 𝑁) ∈ Word 𝑉)) |
4 | 3 | 3ad2ant1 1169 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → ((𝑊 prefix 𝑀) ∈ Word 𝑉 ∧ (𝑈 prefix 𝑁) ∈ Word 𝑉)) |
5 | | eqwrd 13617 |
. . 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 476 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉) |
8 | 7 | 3ad2ant1 1169 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑊 ∈ Word 𝑉) |
9 | | simpl 476 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑀 ∈
ℕ0) |
10 | 9 | 3ad2ant2 1170 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈
ℕ0) |
11 | | lencl 13593 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
12 | 11 | adantr 474 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑊) ∈
ℕ0) |
13 | 12 | 3ad2ant1 1169 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (♯‘𝑊) ∈
ℕ0) |
14 | | simpl 476 |
. . . . . . 7
⊢ ((𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)) → 𝑀 ≤ (♯‘𝑊)) |
15 | 14 | 3ad2ant3 1171 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑀 ≤ (♯‘𝑊)) |
16 | | elfz2nn0 12725 |
. . . . . 6
⊢ (𝑀 ∈
(0...(♯‘𝑊))
↔ (𝑀 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ0 ∧ 𝑀 ≤ (♯‘𝑊))) |
17 | 10, 13, 15, 16 | syl3anbrc 1449 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈ (0...(♯‘𝑊))) |
18 | | pfxlen 13762 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝑀)) = 𝑀) |
19 | 8, 17, 18 | syl2anc 581 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 prefix 𝑀)) = 𝑀) |
20 | | simpr 479 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → 𝑈 ∈ Word 𝑉) |
21 | 20 | 3ad2ant1 1169 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑈 ∈ Word 𝑉) |
22 | | simpr 479 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
23 | 22 | 3ad2ant2 1170 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑁 ∈
ℕ0) |
24 | | lencl 13593 |
. . . . . . . 8
⊢ (𝑈 ∈ Word 𝑉 → (♯‘𝑈) ∈
ℕ0) |
25 | 24 | adantl 475 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑈) ∈
ℕ0) |
26 | 25 | 3ad2ant1 1169 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (♯‘𝑈) ∈
ℕ0) |
27 | | simpr 479 |
. . . . . . 7
⊢ ((𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)) → 𝑁 ≤ (♯‘𝑈)) |
28 | 27 | 3ad2ant3 1171 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑁 ≤ (♯‘𝑈)) |
29 | | elfz2nn0 12725 |
. . . . . 6
⊢ (𝑁 ∈
(0...(♯‘𝑈))
↔ (𝑁 ∈
ℕ0 ∧ (♯‘𝑈) ∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝑈))) |
30 | 23, 26, 28, 29 | syl3anbrc 1449 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑁 ∈ (0...(♯‘𝑈))) |
31 | | pfxlen 13762 |
. . . . 5
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑈))) → (♯‘(𝑈 prefix 𝑁)) = 𝑁) |
32 | 21, 30, 31 | syl2anc 581 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑈 prefix 𝑁)) = 𝑁) |
33 | 19, 32 | eqeq12d 2840 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) →
((♯‘(𝑊 prefix
𝑀)) = (♯‘(𝑈 prefix 𝑁)) ↔ 𝑀 = 𝑁)) |
34 | 33 | anbi1d 625 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) →
(((♯‘(𝑊 prefix
𝑀)) = (♯‘(𝑈 prefix 𝑁)) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)))) |
35 | 8 | adantr 474 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → 𝑊 ∈ Word 𝑉) |
36 | 17 | adantr 474 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → 𝑀 ∈ (0...(♯‘𝑊))) |
37 | 35, 36, 18 | syl2anc 581 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (♯‘(𝑊 prefix 𝑀)) = 𝑀) |
38 | 37 | oveq2d 6921 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (0..^(♯‘(𝑊 prefix 𝑀))) = (0..^𝑀)) |
39 | 38 | raleqdv 3356 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖))) |
40 | 35 | adantr 474 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ Word 𝑉) |
41 | 36 | adantr 474 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ (0...(♯‘𝑊))) |
42 | | simpr 479 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀)) |
43 | | pfxfv 13761 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊)) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑊 prefix 𝑀)‘𝑖) = (𝑊‘𝑖)) |
44 | 40, 41, 42, 43 | syl3anc 1496 |
. . . . . 6
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑊 prefix 𝑀)‘𝑖) = (𝑊‘𝑖)) |
45 | 21 | ad2antrr 719 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑈 ∈ Word 𝑉) |
46 | 30 | ad2antrr 719 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑁 ∈ (0...(♯‘𝑈))) |
47 | | oveq2 6913 |
. . . . . . . . . 10
⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁)) |
48 | 47 | eleq2d 2892 |
. . . . . . . . 9
⊢ (𝑀 = 𝑁 → (𝑖 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑁))) |
49 | 48 | adantl 475 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (𝑖 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑁))) |
50 | 49 | biimpa 470 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑁)) |
51 | | pfxfv 13761 |
. . . . . . 7
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑈 prefix 𝑁)‘𝑖) = (𝑈‘𝑖)) |
52 | 45, 46, 50, 51 | syl3anc 1496 |
. . . . . 6
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑈 prefix 𝑁)‘𝑖) = (𝑈‘𝑖)) |
53 | 44, 52 | eqeq12d 2840 |
. . . . 5
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ (𝑊‘𝑖) = (𝑈‘𝑖))) |
54 | 53 | ralbidva 3194 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^𝑀)((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))) |
55 | 39, 54 | bitrd 271 |
. . 3
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))) |
56 | 55 | pm5.32da 576 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |
57 | 6, 34, 56 | 3bitrd 297 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |