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 1ex 
 |-  1 e. _V
10 9 tpid2 
 |-  1 e. { 0 , 1 , 2 }
11 10 3 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
12 11 5 eleqtrrid 
 |-  ( ( # ` W ) = 3 -> 1 e. ( 0 ..^ ( # ` W ) ) )
13 wrdsymbcl 
 |-  ( ( W e. Word V /\ 1 e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` 1 ) e. V )
14 12 13 sylan2 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( W ` 1 ) e. V )
15 2ex 
 |-  2 e. _V
16 15 tpid3 
 |-  2 e. { 0 , 1 , 2 }
17 16 3 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
18 17 5 eleqtrrid 
 |-  ( ( # ` W ) = 3 -> 2 e. ( 0 ..^ ( # ` W ) ) )
19 wrdsymbcl 
 |-  ( ( W e. Word V /\ 2 e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` 2 ) e. V )
20 18 19 sylan2 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( W ` 2 ) e. V )
21 simpr 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( # ` W ) = 3 )
22 eqid 
 |-  ( W ` 0 ) = ( W ` 0 )
23 eqid 
 |-  ( W ` 1 ) = ( W ` 1 )
24 eqid 
 |-  ( W ` 2 ) = ( W ` 2 )
25 22 23 24 3pm3.2i 
 |-  ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = ( W ` 2 ) )
26 21 25 jctir 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = ( W ` 2 ) ) ) )
27 eqeq2 
 |-  ( a = ( W ` 0 ) -> ( ( W ` 0 ) = a <-> ( W ` 0 ) = ( W ` 0 ) ) )
28 27 3anbi1d 
 |-  ( a = ( W ` 0 ) -> ( ( ( W ` 0 ) = a /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) <-> ( ( W ` 0 ) = ( W ` 0 ) /\ ( W ` 1 ) = b /\ ( W ` 2 ) = c ) ) )
29 28 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 ) ) ) )
30 eqeq2 
 |-  ( b = ( W ` 1 ) -> ( ( W ` 1 ) = b <-> ( W ` 1 ) = ( W ` 1 ) ) )
31 30 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 ) ) )
32 31 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 ) ) ) )
33 eqeq2 
 |-  ( c = ( W ` 2 ) -> ( ( W ` 2 ) = c <-> ( W ` 2 ) = ( W ` 2 ) ) )
34 33 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 ) ) ) )
35 34 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 ) ) ) ) )
36 29 32 35 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 ) ) )
37 8 14 20 26 36 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 ) ) )
38 df-3an 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) <-> ( ( a e. V /\ b e. V ) /\ c e. V ) )
39 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 ) ) ) )
40 39 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 ) ) ) ) )
41 38 40 syl5bir 
 |-  ( 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 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 ) ) ) ) ) )
43 42 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 ) ) ) ) ) )
44 43 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 ) ) ) )
45 44 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 ) ) ) )
46 45 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 ) ) ) )
47 37 46 mpbird 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> E. a e. V E. b e. V E. c e. V W = <" a b c "> )
48 s3cl 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) -> <" a b c "> e. Word V )
49 48 ad4ant123 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ c e. V ) /\ W = <" a b c "> ) -> <" a b c "> e. Word V )
50 s3len 
 |-  ( # ` <" a b c "> ) = 3
51 49 50 jctir 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ c e. V ) /\ W = <" a b c "> ) -> ( <" a b c "> e. Word V /\ ( # ` <" a b c "> ) = 3 ) )
52 eleq1 
 |-  ( W = <" a b c "> -> ( W e. Word V <-> <" a b c "> e. Word V ) )
53 fveqeq2 
 |-  ( W = <" a b c "> -> ( ( # ` W ) = 3 <-> ( # ` <" a b c "> ) = 3 ) )
54 52 53 anbi12d 
 |-  ( W = <" a b c "> -> ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> ( <" a b c "> e. Word V /\ ( # ` <" a b c "> ) = 3 ) ) )
55 54 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 ) ) )
56 51 55 mpbird 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ c e. V ) /\ W = <" a b c "> ) -> ( W e. Word V /\ ( # ` W ) = 3 ) )
57 56 rexlimdva2 
 |-  ( ( a e. V /\ b e. V ) -> ( E. c e. V W = <" a b c "> -> ( W e. Word V /\ ( # ` W ) = 3 ) ) )
58 57 rexlimivv 
 |-  ( E. a e. V E. b e. V E. c e. V W = <" a b c "> -> ( W e. Word V /\ ( # ` W ) = 3 ) )
59 47 58 impbii 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> E. a e. V E. b e. V E. c e. V W = <" a b c "> )