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