Metamath Proof Explorer


Theorem pfxeq

Description: The prefixes of two words are equal iff they have the same length and the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 4-May-2020)

Ref Expression
Assertion pfxeq ( ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝑀 ≤ ( ♯ ‘ 𝑊 ) ∧ 𝑁 ≤ ( ♯ ‘ 𝑈 ) ) ) → ( ( 𝑊 prefix 𝑀 ) = ( 𝑈 prefix 𝑁 ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑊𝑖 ) = ( 𝑈𝑖 ) ) ) )

Proof

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 ..^ 𝑀 ) ( 𝑊𝑖 ) = ( 𝑈𝑖 ) ) ) )