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 
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> E. a e. V E. b e. V E. c e. V W = <" a b c "> )

Proof

Step Hyp Ref Expression
1 c0ex 
 |-  0 e. _V
2 1 tpid1 
 |-  0 e. { 0 , 1 , 2 }
3 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
4 2 3 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
5 oveq2 
 |-  ( ( # ` W ) = 3 -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 3 ) )
6 4 5 eleqtrrid 
 |-  ( ( # ` W ) = 3 -> 0 e. ( 0 ..^ ( # ` W ) ) )
7 wrdsymbcl 
 |-  ( ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` 0 ) e. V )
8 6 7 sylan2 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( W ` 0 ) e. V )
9 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
10 9 3 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
11 10 5 eleqtrrid 
 |-  ( ( # ` W ) = 3 -> 1 e. ( 0 ..^ ( # ` W ) ) )
12 wrdsymbcl 
 |-  ( ( W e. Word V /\ 1 e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` 1 ) e. V )
13 11 12 sylan2 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( W ` 1 ) e. V )
14 2ex 
 |-  2 e. _V
15 14 tpid3 
 |-  2 e. { 0 , 1 , 2 }
16 15 3 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
17 16 5 eleqtrrid 
 |-  ( ( # ` W ) = 3 -> 2 e. ( 0 ..^ ( # ` W ) ) )
18 wrdsymbcl 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` 2 ) e. V )
19 17 18 sylan2 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( W ` 2 ) e. V )
20 simpr 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( # ` W ) = 3 )
21 eqid 
 |-  ( W ` 0 ) = ( W ` 0 )
22 eqid 
 |-  ( W ` 1 ) = ( W ` 1 )
23 eqid 
 |-  ( W ` 2 ) = ( W ` 2 )
24 21 22 23 3pm3.2i 
 |-  ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = ( W ` 2 ) )
25 20 24 jctir 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = ( W ` 2 ) ) ) )
26 eqeq2 
 |-  ( a = ( W ` 0 ) -> ( ( W ` 0 ) = a <-> ( W ` 0 ) = ( W ` 0 ) ) )
27 26 3anbi1d 
 |-  ( a = ( W ` 0 ) -> ( ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) <-> ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) )
28 27 anbi2d 
 |-  ( a = ( W ` 0 ) -> ( ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) )
29 eqeq2 
 |-  ( b = ( W ` 1 ) -> ( ( W ` 1 ) = b <-> ( W ` 1 ) = ( W ` 1 ) ) )
30 29 3anbi2d 
 |-  ( b = ( W ` 1 ) -> ( ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) <-> ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = c ) ) )
31 30 anbi2d 
 |-  ( b = ( W ` 1 ) -> ( ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = c ) ) ) )
32 eqeq2 
 |-  ( c = ( W ` 2 ) -> ( ( W ` 2 ) = c <-> ( W ` 2 ) = ( W ` 2 ) ) )
33 32 3anbi3d 
 |-  ( c = ( W ` 2 ) -> ( ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = c ) <-> ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = ( W ` 2 ) ) ) )
34 33 anbi2d 
 |-  ( c = ( W ` 2 ) -> ( ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = c ) ) <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = ( W ` 2 ) ) ) ) )
35 28 31 34 rspc3ev 
 |-  ( ( ( ( W ` 0 ) e. V /\ ( W ` 1 ) e. V /\ ( W ` 2 ) e. V ) /\ ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = ( W ` 2 ) ) ) ) -> E. a e. V E. b e. V E. c e. V ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) )
36 8 13 19 25 35 syl31anc 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) )
37 df-3an 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) <-> ( ( a e. V /\ b e. V ) /\ c e. V ) )
38 eqwrds3 
 |-  ( ( W e. Word V /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( W = <" a b c "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) )
39 38 ex 
 |-  ( W e. Word V -> ( ( a e. V /\ b e. V /\ c e. V ) -> ( W = <" a b c "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) ) )
40 37 39 biimtrrid 
 |-  ( W e. Word V -> ( ( ( a e. V /\ b e. V ) /\ c e. V ) -> ( W = <" a b c "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) ) )
41 40 expd 
 |-  ( W e. Word V -> ( ( a e. V /\ b e. V ) -> ( c e. V -> ( W = <" a b c "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) ) ) )
42 41 adantr 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( ( a e. V /\ b e. V ) -> ( c e. V -> ( W = <" a b c "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) ) ) )
43 42 imp31 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) = 3 ) /\ ( a e. V /\ b e. V ) ) /\ c e. V ) -> ( W = <" a b c "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) )
44 43 rexbidva 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = 3 ) /\ ( a e. V /\ b e. V ) ) -> ( E. c e. V W = <" a b c "> <-> E. c e. V ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) )
45 44 2rexbidva 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( E. a e. V E. b e. V E. c e. V W = <" a b c "> <-> E. a e. V E. b e. V E. c e. V ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) ) )
46 36 45 mpbird 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> E. a e. V E. b e. V E. c e. V W = <" a b c "> )
47 s3cl 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) -> <" a b c "> e. Word V )
48 47 ad4ant123 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ c e. V ) /\ W = <" a b c "> ) -> <" a b c "> e. Word V )
49 s3len 
 |-  ( # ` <" a b c "> ) = 3
50 48 49 jctir 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ c e. V ) /\ W = <" a b c "> ) -> ( <" a b c "> e. Word V /\ ( # ` <" a b c "> ) = 3 ) )
51 eleq1 
 |-  ( W = <" a b c "> -> ( W e. Word V <-> <" a b c "> e. Word V ) )
52 fveqeq2 
 |-  ( W = <" a b c "> -> ( ( # ` W ) = 3 <-> ( # ` <" a b c "> ) = 3 ) )
53 51 52 anbi12d 
 |-  ( W = <" a b c "> -> ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> ( <" a b c "> e. Word V /\ ( # ` <" a b c "> ) = 3 ) ) )
54 53 adantl 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ c e. V ) /\ W = <" a b c "> ) -> ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> ( <" a b c "> e. Word V /\ ( # ` <" a b c "> ) = 3 ) ) )
55 50 54 mpbird 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ c e. V ) /\ W = <" a b c "> ) -> ( W e. Word V /\ ( # ` W ) = 3 ) )
56 55 rexlimdva2 
 |-  ( ( a e. V /\ b e. V ) -> ( E. c e. V W = <" a b c "> -> ( W e. Word V /\ ( # ` W ) = 3 ) ) )
57 56 rexlimivv 
 |-  ( E. a e. V E. b e. V E. c e. V W = <" a b c "> -> ( W e. Word V /\ ( # ` W ) = 3 ) )
58 46 57 impbii 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> E. a e. V E. b e. V E. c e. V W = <" a b c "> )