Theorem wrdpmcl

Description: Closure of a word with permuted symbols. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	wrdpmcl.1	|- J = ( 0 ..^ ( # ` W ) )
	wrdpmcl.2	|- ( ph -> E : J -1-1-onto-> J )
	wrdpmcl.3	|- ( ph -> W e. Word S )
Assertion	wrdpmcl	|- ( ph -> ( W o. E ) e. Word S )

Proof

Step	Hyp	Ref	Expression
1		wrdpmcl.1	|- J = ( 0 ..^ ( # ` W ) )
2		wrdpmcl.2	|- ( ph -> E : J -1-1-onto-> J )
3		wrdpmcl.3	|- ( ph -> W e. Word S )
4		eqidd	|- ( ph -> ( # ` W ) = ( # ` W ) )
5	4 3	wrdfd	|- ( ph -> W : ( 0 ..^ ( # ` W ) ) --> S )
6		f1oeq23	|- ( ( J = ( 0 ..^ ( # ` W ) ) /\ J = ( 0 ..^ ( # ` W ) ) ) -> ( E : J -1-1-onto-> J <-> E : ( 0 ..^ ( # ` W ) ) -1-1-onto-> ( 0 ..^ ( # ` W ) ) ) )
7	1 1 6	mp2an	|- ( E : J -1-1-onto-> J <-> E : ( 0 ..^ ( # ` W ) ) -1-1-onto-> ( 0 ..^ ( # ` W ) ) )
8	2 7	sylib	|- ( ph -> E : ( 0 ..^ ( # ` W ) ) -1-1-onto-> ( 0 ..^ ( # ` W ) ) )
9		f1of	|- ( E : ( 0 ..^ ( # ` W ) ) -1-1-onto-> ( 0 ..^ ( # ` W ) ) -> E : ( 0 ..^ ( # ` W ) ) --> ( 0 ..^ ( # ` W ) ) )
10	8 9	syl	|- ( ph -> E : ( 0 ..^ ( # ` W ) ) --> ( 0 ..^ ( # ` W ) ) )
11	5 10	fcod	|- ( ph -> ( W o. E ) : ( 0 ..^ ( # ` W ) ) --> S )
12		iswrdi	|- ( ( W o. E ) : ( 0 ..^ ( # ` W ) ) --> S -> ( W o. E ) e. Word S )
13	11 12	syl	|- ( ph -> ( W o. E ) e. Word S )