Theorem wrdsymb

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

	Ref	Expression
Assertion	wrdsymb	$$⊢S\in \mathrm{Word}A\to S\in \mathrm{Word}S\left[\left(0..^\left|S\right|\right)\right]$$

Proof

Step	Hyp	Ref	Expression
1		wrdf	$$⊢S\in \mathrm{Word}A\to S:\left(0..^\left|S\right|\right)⟶A$$
2		fimadmfo	$$⊢S:\left(0..^\left|S\right|\right)⟶A\to S:\left(0..^\left|S\right|\right)\underset{onto}{⟶}S\left[\left(0..^\left|S\right|\right)\right]$$
3		fof	$$⊢S:\left(0..^\left|S\right|\right)\underset{onto}{⟶}S\left[\left(0..^\left|S\right|\right)\right]\to S:\left(0..^\left|S\right|\right)⟶S\left[\left(0..^\left|S\right|\right)\right]$$
4	1 2 3	3syl	$$⊢S\in \mathrm{Word}A\to S:\left(0..^\left|S\right|\right)⟶S\left[\left(0..^\left|S\right|\right)\right]$$
5		iswrdb	$$⊢S\in \mathrm{Word}S\left[\left(0..^\left|S\right|\right)\right]\leftrightarrow S:\left(0..^\left|S\right|\right)⟶S\left[\left(0..^\left|S\right|\right)\right]$$
6	4 5	sylibr	$$⊢S\in \mathrm{Word}A\to S\in \mathrm{Word}S\left[\left(0..^\left|S\right|\right)\right]$$