Theorem fstwrdne

Description: The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 28-Sep-2018) (Proof shortened by AV, 14-Oct-2018)

	Ref	Expression
Assertion	fstwrdne	$$⊢\left(W\in \mathrm{Word}V\wedge W\ne \varnothing \right)\to W\left(0\right)\in V$$

Proof

Step	Hyp	Ref	Expression
1		wrdlenge1n0	$$⊢W\in \mathrm{Word}V\to \left(W\ne \varnothing \leftrightarrow 1\le \left|W\right|\right)$$
2		wrdsymb1	$$⊢\left(W\in \mathrm{Word}V\wedge 1\le \left|W\right|\right)\to W\left(0\right)\in V$$
3	2	ex	$$⊢W\in \mathrm{Word}V\to \left(1\le \left|W\right|\to W\left(0\right)\in V\right)$$
4	1 3	sylbid	$$⊢W\in \mathrm{Word}V\to \left(W\ne \varnothing \to W\left(0\right)\in V\right)$$
5	4	imp	$$⊢\left(W\in \mathrm{Word}V\wedge W\ne \varnothing \right)\to W\left(0\right)\in V$$