This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑆 )