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 ..^ ( ♯ ‘ 𝑆 ) ) ) )