Theorem wrdpmcl

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

	Ref	Expression
Hypotheses	wrdpmcl.1	⊢ 𝐽 = ( 0 ..^ ( ♯ ‘ 𝑊 ) )
	wrdpmcl.2	⊢ ( 𝜑 → 𝐸 : 𝐽 –1-1-onto→ 𝐽 )
	wrdpmcl.3	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
Assertion	wrdpmcl	⊢ ( 𝜑 → ( 𝑊 ∘ 𝐸 ) ∈ Word 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		wrdpmcl.1	⊢ 𝐽 = ( 0 ..^ ( ♯ ‘ 𝑊 ) )
2		wrdpmcl.2	⊢ ( 𝜑 → 𝐸 : 𝐽 –1-1-onto→ 𝐽 )
3		wrdpmcl.3	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
4		eqidd	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
5	4 3	wrdfd	⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
6		f1oeq23	⊢ ( ( 𝐽 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐽 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐸 : 𝐽 –1-1-onto→ 𝐽 ↔ 𝐸 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
7	1 1 6	mp2an	⊢ ( 𝐸 : 𝐽 –1-1-onto→ 𝐽 ↔ 𝐸 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
8	2 7	sylib	⊢ ( 𝜑 → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9		f1of	⊢ ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10	8 9	syl	⊢ ( 𝜑 → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11	5 10	fcod	⊢ ( 𝜑 → ( 𝑊 ∘ 𝐸 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
12		iswrdi	⊢ ( ( 𝑊 ∘ 𝐸 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 → ( 𝑊 ∘ 𝐸 ) ∈ Word 𝑆 )
13	11 12	syl	⊢ ( 𝜑 → ( 𝑊 ∘ 𝐸 ) ∈ Word 𝑆 )