Metamath Proof Explorer

Theorem wrdlen3s3

Description: A word of length three as length 3 string. (Contributed by AV, 26-Jan-2021)

Ref Expression
Assertion wrdlen3s3 
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) -> W = <" ( W ` 0 ) ( W ` 1 ) ( W ` 2 ) "> )

Proof

Step Hyp Ref Expression
1 wrd3tpop 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> W = { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. , <. 2 , ( W ` 2 ) >. } )
2 fvex 
 |-  ( W ` 0 ) e. _V
3 fvex 
 |-  ( W ` 1 ) e. _V
4 fvex 
 |-  ( W ` 2 ) e. _V
5 s3tpop 
 |-  ( ( ( W ` 0 ) e. _V /\ ( W ` 1 ) e. _V /\ ( W ` 2 ) e. _V ) -> <" ( W ` 0 ) ( W ` 1 ) ( W ` 2 ) "> = { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. , <. 2 , ( W ` 2 ) >. } )
6 5 eqcomd 
 |-  ( ( ( W ` 0 ) e. _V /\ ( W ` 1 ) e. _V /\ ( W ` 2 ) e. _V ) -> { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. , <. 2 , ( W ` 2 ) >. } = <" ( W ` 0 ) ( W ` 1 ) ( W ` 2 ) "> )
7 2 3 4 6 mp3an 
 |-  { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. , <. 2 , ( W ` 2 ) >. } = <" ( W ` 0 ) ( W ` 1 ) ( W ` 2 ) ">
8 1 7 eqtrdi 
 |-  ( ( W e. Word V /\ ( # ` W ) = 3 ) -> W = <" ( W ` 0 ) ( W ` 1 ) ( W ` 2 ) "> )