Metamath Proof Explorer

Theorem pfx2

Description: A prefix of length two. (Contributed by AV, 15-May-2020)

Ref Expression
Assertion pfx2 ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix 2 ) = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ )

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ0
2 1 a1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ∈ ℕ0 )
3 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 3 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
5 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
6 elfz2nn0 ⊢ ( 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 2 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
7 2 4 5 6 syl3anbrc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
8 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 )
9 s2len ⊢ ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) = 2
10 9 eqcomi ⊢ 2 = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ )
11 10 a1i ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 ) → 2 = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) )
12 2nn ⊢ 2 ∈ ℕ
13 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ 2 ∈ ℕ )
14 12 13 mpbir ⊢ 0 ∈ ( 0 ..^ 2 )
15 pfxfv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 0 ∈ ( 0 ..^ 2 ) ) → ( ( 𝑊 prefix 2 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
16 14 15 mp3an3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 2 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
17 16 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 ) → ( ( 𝑊 prefix 2 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
18 fvex ⊢ ( 𝑊 ‘ 0 ) ∈ V
19 s2fv0 ⊢ ( ( 𝑊 ‘ 0 ) ∈ V → ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 0 ) = ( 𝑊 ‘ 0 ) )
20 18 19 ax-mp ⊢ ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 0 ) = ( 𝑊 ‘ 0 )
21 17 20 eqtr4di ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 ) → ( ( 𝑊 prefix 2 ) ‘ 0 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 0 ) )
22 1nn0 ⊢ 1 ∈ ℕ0
23 1lt2 ⊢ 1 < 2
24 elfzo0 ⊢ ( 1 ∈ ( 0 ..^ 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2 ) )
25 22 12 23 24 mpbir3an ⊢ 1 ∈ ( 0 ..^ 2 )
26 pfxfv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 1 ∈ ( 0 ..^ 2 ) ) → ( ( 𝑊 prefix 2 ) ‘ 1 ) = ( 𝑊 ‘ 1 ) )
27 25 26 mp3an3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 2 ) ‘ 1 ) = ( 𝑊 ‘ 1 ) )
28 fvex ⊢ ( 𝑊 ‘ 1 ) ∈ V
29 s2fv1 ⊢ ( ( 𝑊 ‘ 1 ) ∈ V → ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 1 ) = ( 𝑊 ‘ 1 ) )
30 28 29 ax-mp ⊢ ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 1 ) = ( 𝑊 ‘ 1 )
31 27 30 eqtr4di ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 2 ) ‘ 1 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 1 ) )
32 31 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 ) → ( ( 𝑊 prefix 2 ) ‘ 1 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 1 ) )
33 0nn0 ⊢ 0 ∈ ℕ0
34 fveq2 ⊢ ( 𝑖 = 0 → ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ( 𝑊 prefix 2 ) ‘ 0 ) )
35 fveq2 ⊢ ( 𝑖 = 0 → ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 0 ) )
36 34 35 eqeq12d ⊢ ( 𝑖 = 0 → ( ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ↔ ( ( 𝑊 prefix 2 ) ‘ 0 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 0 ) ) )
37 fveq2 ⊢ ( 𝑖 = 1 → ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ( 𝑊 prefix 2 ) ‘ 1 ) )
38 fveq2 ⊢ ( 𝑖 = 1 → ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 1 ) )
39 37 38 eqeq12d ⊢ ( 𝑖 = 1 → ( ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ↔ ( ( 𝑊 prefix 2 ) ‘ 1 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 1 ) ) )
40 36 39 ralprg ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ { 0 , 1 } ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ↔ ( ( ( 𝑊 prefix 2 ) ‘ 0 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 0 ) ∧ ( ( 𝑊 prefix 2 ) ‘ 1 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 1 ) ) ) )
41 33 22 40 mp2an ⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ↔ ( ( ( 𝑊 prefix 2 ) ‘ 0 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 0 ) ∧ ( ( 𝑊 prefix 2 ) ‘ 1 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 1 ) ) )
42 21 32 41 sylanbrc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 ) → ∀ 𝑖 ∈ { 0 , 1 } ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) )
43 eqeq1 ⊢ ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 → ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ↔ 2 = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ) )
44 oveq2 ⊢ ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 → ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) = ( 0 ..^ 2 ) )
45 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
46 44 45 eqtrdi ⊢ ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 → ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) = { 0 , 1 } )
47 46 raleqdv ⊢ ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ { 0 , 1 } ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) )
48 43 47 anbi12d ⊢ ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 → ( ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) ↔ ( 2 = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ { 0 , 1 } ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) ) )
49 48 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 ) → ( ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) ↔ ( 2 = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ { 0 , 1 } ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) ) )
50 11 42 49 mpbir2and ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ ( ♯ ‘ ( 𝑊 prefix 2 ) ) = 2 ) → ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) )
51 8 50 mpdan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) )
52 pfxcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 2 ) ∈ Word 𝑉 )
53 s2cli ⊢ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ∈ Word V
54 eqwrd ⊢ ( ( ( 𝑊 prefix 2 ) ∈ Word 𝑉 ∧ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ∈ Word V ) → ( ( 𝑊 prefix 2 ) = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ↔ ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) ) )
55 52 53 54 sylancl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 prefix 2 ) = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ↔ ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) ) )
56 55 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 2 ) = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ↔ ( ( ♯ ‘ ( 𝑊 prefix 2 ) ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 2 ) ) ) ( ( 𝑊 prefix 2 ) ‘ 𝑖 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ‘ 𝑖 ) ) ) )
57 51 56 mpbird ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 2 ) = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ )
58 7 57 syldan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix 2 ) = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ )