Metamath Proof Explorer

Theorem pfx2

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

Ref Expression
Assertion pfx2 ⊢W∈WordV∧2≤W→Wprefix2=⟨“W⁡0W⁡1”⟩

Proof

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