Description: A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | wrdl3s3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0ex | |
|
2 | 1 | tpid1 | |
3 | fzo0to3tp | |
|
4 | 2 3 | eleqtrri | |
5 | oveq2 | |
|
6 | 4 5 | eleqtrrid | |
7 | wrdsymbcl | |
|
8 | 6 7 | sylan2 | |
9 | 1ex | |
|
10 | 9 | tpid2 | |
11 | 10 3 | eleqtrri | |
12 | 11 5 | eleqtrrid | |
13 | wrdsymbcl | |
|
14 | 12 13 | sylan2 | |
15 | 2ex | |
|
16 | 15 | tpid3 | |
17 | 16 3 | eleqtrri | |
18 | 17 5 | eleqtrrid | |
19 | wrdsymbcl | |
|
20 | 18 19 | sylan2 | |
21 | simpr | |
|
22 | eqid | |
|
23 | eqid | |
|
24 | eqid | |
|
25 | 22 23 24 | 3pm3.2i | |
26 | 21 25 | jctir | |
27 | eqeq2 | |
|
28 | 27 | 3anbi1d | |
29 | 28 | anbi2d | |
30 | eqeq2 | |
|
31 | 30 | 3anbi2d | |
32 | 31 | anbi2d | |
33 | eqeq2 | |
|
34 | 33 | 3anbi3d | |
35 | 34 | anbi2d | |
36 | 29 32 35 | rspc3ev | |
37 | 8 14 20 26 36 | syl31anc | |
38 | df-3an | |
|
39 | eqwrds3 | |
|
40 | 39 | ex | |
41 | 38 40 | syl5bir | |
42 | 41 | expd | |
43 | 42 | adantr | |
44 | 43 | imp31 | |
45 | 44 | rexbidva | |
46 | 45 | 2rexbidva | |
47 | 37 46 | mpbird | |
48 | s3cl | |
|
49 | 48 | ad4ant123 | |
50 | s3len | |
|
51 | 49 50 | jctir | |
52 | eleq1 | |
|
53 | fveqeq2 | |
|
54 | 52 53 | anbi12d | |
55 | 54 | adantl | |
56 | 51 55 | mpbird | |
57 | 56 | rexlimdva2 | |
58 | 57 | rexlimivv | |
59 | 47 58 | impbii | |