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

Metamath Proof Explorer

Theorem wrdsymb

Description: A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022)

Ref Expression
Assertion wrdsymb ( 𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word ( 𝑆 “ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 wrdf ⊢ ( 𝑆 ∈ Word 𝐴 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
2 fimadmfo ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) –onto→ ( 𝑆 “ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
3 fof ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) –onto→ ( 𝑆 “ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ ( 𝑆 “ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
4 1 2 3 3syl ⊢ ( 𝑆 ∈ Word 𝐴 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ ( 𝑆 “ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
5 iswrdb ⊢ ( 𝑆 ∈ Word ( 𝑆 “ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ↔ 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ ( 𝑆 “ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
6 4 5 sylibr ⊢ ( 𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word ( 𝑆 “ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )