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