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