Theorem wrdpmcl

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

	Ref	Expression
Hypotheses	wrdpmcl.1	$$⊢J=\left(0..^\left|W\right|\right)$$
	wrdpmcl.2	$$⊢\phi \to E:J\underset{1-1\; onto}{⟶}J$$
	wrdpmcl.3	$$⊢\phi \to W\in \mathrm{Word}S$$
Assertion	wrdpmcl	$$⊢\phi \to W\circ E\in \mathrm{Word}S$$

Proof

Step	Hyp	Ref	Expression
1		wrdpmcl.1	$$⊢J=\left(0..^\left|W\right|\right)$$
2		wrdpmcl.2	$$⊢\phi \to E:J\underset{1-1\; onto}{⟶}J$$
3		wrdpmcl.3	$$⊢\phi \to W\in \mathrm{Word}S$$
4		eqidd	$$⊢\phi \to \left|W\right|=\left|W\right|$$
5	4 3	wrdfd	$$⊢\phi \to W:\left(0..^\left|W\right|\right)⟶S$$
6		f1oeq23	$$⊢\left(J=\left(0..^\left|W\right|\right)\wedge J=\left(0..^\left|W\right|\right)\right)\to \left(E:J\underset{1-1\; onto}{⟶}J\leftrightarrow E:\left(0..^\left|W\right|\right)\underset{1-1\; onto}{⟶}\left(0..^\left|W\right|\right)\right)$$
7	1 1 6	mp2an	$$⊢E:J\underset{1-1\; onto}{⟶}J\leftrightarrow E:\left(0..^\left|W\right|\right)\underset{1-1\; onto}{⟶}\left(0..^\left|W\right|\right)$$
8	2 7	sylib	$$⊢\phi \to E:\left(0..^\left|W\right|\right)\underset{1-1\; onto}{⟶}\left(0..^\left|W\right|\right)$$
9		f1of	$$⊢E:\left(0..^\left|W\right|\right)\underset{1-1\; onto}{⟶}\left(0..^\left|W\right|\right)\to E:\left(0..^\left|W\right|\right)⟶\left(0..^\left|W\right|\right)$$
10	8 9	syl	$$⊢\phi \to E:\left(0..^\left|W\right|\right)⟶\left(0..^\left|W\right|\right)$$
11	5 10	fcod	$$⊢\phi \to \left(W\circ E\right):\left(0..^\left|W\right|\right)⟶S$$
12		iswrdi	$$⊢\left(W\circ E\right):\left(0..^\left|W\right|\right)⟶S\to W\circ E\in \mathrm{Word}S$$
13	11 12	syl	$$⊢\phi \to W\circ E\in \mathrm{Word}S$$