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 ) "> )