Metamath Proof Explorer


Theorem wrdl3s3

Description: A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021)

Ref Expression
Assertion wrdl3s3 WWordVW=3aVbVcVW=⟨“abc”⟩

Proof

Step Hyp Ref Expression
1 c0ex 0V
2 1 tpid1 0012
3 fzo0to3tp 0..^3=012
4 2 3 eleqtrri 00..^3
5 oveq2 W=30..^W=0..^3
6 4 5 eleqtrrid W=300..^W
7 wrdsymbcl WWordV00..^WW0V
8 6 7 sylan2 WWordVW=3W0V
9 1ex 1V
10 9 tpid2 1012
11 10 3 eleqtrri 10..^3
12 11 5 eleqtrrid W=310..^W
13 wrdsymbcl WWordV10..^WW1V
14 12 13 sylan2 WWordVW=3W1V
15 2ex 2V
16 15 tpid3 2012
17 16 3 eleqtrri 20..^3
18 17 5 eleqtrrid W=320..^W
19 wrdsymbcl WWordV20..^WW2V
20 18 19 sylan2 WWordVW=3W2V
21 simpr WWordVW=3W=3
22 eqid W0=W0
23 eqid W1=W1
24 eqid W2=W2
25 22 23 24 3pm3.2i W0=W0W1=W1W2=W2
26 21 25 jctir WWordVW=3W=3W0=W0W1=W1W2=W2
27 eqeq2 a=W0W0=aW0=W0
28 27 3anbi1d a=W0W0=aW1=bW2=cW0=W0W1=bW2=c
29 28 anbi2d a=W0W=3W0=aW1=bW2=cW=3W0=W0W1=bW2=c
30 eqeq2 b=W1W1=bW1=W1
31 30 3anbi2d b=W1W0=W0W1=bW2=cW0=W0W1=W1W2=c
32 31 anbi2d b=W1W=3W0=W0W1=bW2=cW=3W0=W0W1=W1W2=c
33 eqeq2 c=W2W2=cW2=W2
34 33 3anbi3d c=W2W0=W0W1=W1W2=cW0=W0W1=W1W2=W2
35 34 anbi2d c=W2W=3W0=W0W1=W1W2=cW=3W0=W0W1=W1W2=W2
36 29 32 35 rspc3ev W0VW1VW2VW=3W0=W0W1=W1W2=W2aVbVcVW=3W0=aW1=bW2=c
37 8 14 20 26 36 syl31anc WWordVW=3aVbVcVW=3W0=aW1=bW2=c
38 df-3an aVbVcVaVbVcV
39 eqwrds3 WWordVaVbVcVW=⟨“abc”⟩W=3W0=aW1=bW2=c
40 39 ex WWordVaVbVcVW=⟨“abc”⟩W=3W0=aW1=bW2=c
41 38 40 syl5bir WWordVaVbVcVW=⟨“abc”⟩W=3W0=aW1=bW2=c
42 41 expd WWordVaVbVcVW=⟨“abc”⟩W=3W0=aW1=bW2=c
43 42 adantr WWordVW=3aVbVcVW=⟨“abc”⟩W=3W0=aW1=bW2=c
44 43 imp31 WWordVW=3aVbVcVW=⟨“abc”⟩W=3W0=aW1=bW2=c
45 44 rexbidva WWordVW=3aVbVcVW=⟨“abc”⟩cVW=3W0=aW1=bW2=c
46 45 2rexbidva WWordVW=3aVbVcVW=⟨“abc”⟩aVbVcVW=3W0=aW1=bW2=c
47 37 46 mpbird WWordVW=3aVbVcVW=⟨“abc”⟩
48 s3cl aVbVcV⟨“abc”⟩WordV
49 48 ad4ant123 aVbVcVW=⟨“abc”⟩⟨“abc”⟩WordV
50 s3len ⟨“abc”⟩=3
51 49 50 jctir aVbVcVW=⟨“abc”⟩⟨“abc”⟩WordV⟨“abc”⟩=3
52 eleq1 W=⟨“abc”⟩WWordV⟨“abc”⟩WordV
53 fveqeq2 W=⟨“abc”⟩W=3⟨“abc”⟩=3
54 52 53 anbi12d W=⟨“abc”⟩WWordVW=3⟨“abc”⟩WordV⟨“abc”⟩=3
55 54 adantl aVbVcVW=⟨“abc”⟩WWordVW=3⟨“abc”⟩WordV⟨“abc”⟩=3
56 51 55 mpbird aVbVcVW=⟨“abc”⟩WWordVW=3
57 56 rexlimdva2 aVbVcVW=⟨“abc”⟩WWordVW=3
58 57 rexlimivv aVbVcVW=⟨“abc”⟩WWordVW=3
59 47 58 impbii WWordVW=3aVbVcVW=⟨“abc”⟩