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	|- ( ( W e. Word V /\ W =/= (/) ) -> ( W ` 0 ) e. V )

Proof

Step	Hyp	Ref	Expression
1		wrdlenge1n0	|- ( W e. Word V -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) )
2		wrdsymb1	|- ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. V )
3	2	ex	|- ( W e. Word V -> ( 1 <_ ( # ` W ) -> ( W ` 0 ) e. V ) )
4	1 3	sylbid	|- ( W e. Word V -> ( W =/= (/) -> ( W ` 0 ) e. V ) )
5	4	imp	|- ( ( W e. Word V /\ W =/= (/) ) -> ( W ` 0 ) e. V )