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