Metamath Proof Explorer


Theorem wrdlen2s2

Description: A word of length two as doubleton word. (Contributed by AV, 20-Oct-2018)

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

Proof

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