Theorem pmtrdifwrdellem1

Description: Lemma 1 for pmtrdifwrdel . (Contributed by AV, 15-Jan-2019)

	Ref	Expression
Hypotheses	pmtrdifel.t	|- T = ran ( pmTrsp ` ( N \ { K } ) )
	pmtrdifel.r	|- R = ran ( pmTrsp ` N )
	pmtrdifwrdel.0	|- U = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) )
Assertion	pmtrdifwrdellem1	|- ( W e. Word T -> U e. Word R )

Proof

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 )