Step |
Hyp |
Ref |
Expression |
1 |
|
pfxcl |
⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝑀 ) ∈ Word 𝑉 ) |
2 |
|
pfxcl |
⊢ ( 𝑈 ∈ Word 𝑉 → ( 𝑈 prefix 𝑁 ) ∈ Word 𝑉 ) |
3 |
|
eqwrd |
⊢ ( ( ( 𝑊 prefix 𝑀 ) ∈ Word 𝑉 ∧ ( 𝑈 prefix 𝑁 ) ∈ Word 𝑉 ) → ( ( 𝑊 prefix 𝑀 ) = ( 𝑈 prefix 𝑁 ) ↔ ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = ( ♯ ‘ ( 𝑈 prefix 𝑁 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ) ) ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) → ( ( 𝑊 prefix 𝑀 ) = ( 𝑈 prefix 𝑁 ) ↔ ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = ( ♯ ‘ ( 𝑈 prefix 𝑁 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ) ) ) |
5 |
4
|
3ad2ant2 |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑊 prefix 𝑀 ) = ( 𝑈 prefix 𝑁 ) ↔ ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = ( ♯ ‘ ( 𝑈 prefix 𝑁 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ) ) ) |
6 |
|
simp2l |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → 𝑊 ∈ Word 𝑉 ) |
7 |
|
simpl |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 ) |
8 |
|
lencl |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
9 |
8
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
10 |
|
simpl |
⊢ ( ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) → 𝑀 ≤ ( ♯ ‘ 𝑊 ) ) |
11 |
7 9 10
|
3anim123i |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( 𝑀 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑀 ≤ ( ♯ ‘ 𝑊 ) ) ) |
12 |
|
elfz2nn0 |
⊢ ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑀 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑀 ≤ ( ♯ ‘ 𝑊 ) ) ) |
13 |
11 12
|
sylibr |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
14 |
|
pfxlen |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = 𝑀 ) |
15 |
6 13 14
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = 𝑀 ) |
16 |
|
simp2r |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → 𝑈 ∈ Word 𝑉 ) |
17 |
|
simpr |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 ) |
18 |
|
lencl |
⊢ ( 𝑈 ∈ Word 𝑉 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) |
19 |
18
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) |
20 |
|
simpr |
⊢ ( ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) → 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) |
21 |
17 19 20
|
3anim123i |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) |
22 |
|
elfz2nn0 |
⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑈 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) |
23 |
21 22
|
sylibr |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑈 ) ) ) |
24 |
|
pfxlen |
⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑈 ) ) ) → ( ♯ ‘ ( 𝑈 prefix 𝑁 ) ) = 𝑁 ) |
25 |
16 23 24
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ♯ ‘ ( 𝑈 prefix 𝑁 ) ) = 𝑁 ) |
26 |
15 25
|
eqeq12d |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = ( ♯ ‘ ( 𝑈 prefix 𝑁 ) ) ↔ 𝑀 = 𝑁 ) ) |
27 |
26
|
anbi1d |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = ( ♯ ‘ ( 𝑈 prefix 𝑁 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ) ) ) |
28 |
15
|
adantr |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = 𝑀 ) |
29 |
28
|
oveq2d |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) = ( 0 ..^ 𝑀 ) ) |
30 |
29
|
raleqdv |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ) ) |
31 |
6
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ Word 𝑉 ) |
32 |
13
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
33 |
|
simpr |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) ) |
34 |
|
pfxfv |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) |
35 |
31 32 33 34
|
syl3anc |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) |
36 |
16
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑈 ∈ Word 𝑉 ) |
37 |
23
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑈 ) ) ) |
38 |
|
oveq2 |
⊢ ( 𝑀 = 𝑁 → ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ) |
39 |
38
|
eleq2d |
⊢ ( 𝑀 = 𝑁 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ) |
40 |
39
|
adantl |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ) |
41 |
40
|
biimpa |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) ) |
42 |
|
pfxfv |
⊢ ( ( 𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑈 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) |
43 |
36 37 41 42
|
syl3anc |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) |
44 |
35 43
|
eqeq12d |
⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ↔ ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) |
45 |
44
|
ralbidva |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) |
46 |
30 45
|
bitrd |
⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) |
47 |
46
|
pm5.32da |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) ( ( 𝑊 prefix 𝑀 ) ‘ 𝑖 ) = ( ( 𝑈 prefix 𝑁 ) ‘ 𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) ) |
48 |
5 27 47
|
3bitrd |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑊 prefix 𝑀 ) = ( 𝑈 prefix 𝑁 ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) ) |
49 |
48
|
3com12 |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑊 prefix 𝑀 ) = ( 𝑈 prefix 𝑁 ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑊 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) ) |