| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pmtrdifel.t |
|- T = ran ( pmTrsp ` ( N \ { K } ) ) |
| 2 |
|
pmtrdifel.r |
|- R = ran ( pmTrsp ` N ) |
| 3 |
|
pmtrdifwrdel.0 |
|- U = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) ) |
| 4 |
|
wrdsymbcl |
|- ( ( W e. Word T /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` x ) e. T ) |
| 5 |
|
eqid |
|- ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) |
| 6 |
1 2 5
|
pmtrdifellem1 |
|- ( ( W ` x ) e. T -> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) e. R ) |
| 7 |
4 6
|
syl |
|- ( ( W e. Word T /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) e. R ) |
| 8 |
7 3
|
fmptd |
|- ( W e. Word T -> U : ( 0 ..^ ( # ` W ) ) --> R ) |
| 9 |
|
iswrdi |
|- ( U : ( 0 ..^ ( # ` W ) ) --> R -> U e. Word R ) |
| 10 |
8 9
|
syl |
|- ( W e. Word T -> U e. Word R ) |