Theorem wrdsymb1

Description: The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018)

	Ref	Expression
Assertion	wrdsymb1	|- ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. V )

Proof

Step	Hyp	Ref	Expression
1		lencl	|- ( W e. Word V -> ( # ` W ) e. NN0 )
2		elnnnn0c	|- ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ 1 <_ ( # ` W ) ) )
3	2	biimpri	|- ( ( ( # ` W ) e. NN0 /\ 1 <_ ( # ` W ) ) -> ( # ` W ) e. NN )
4	1 3	sylan	|- ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( # ` W ) e. NN )
5		lbfzo0	|- ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN )
6	4 5	sylibr	|- ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
7		wrdsymbcl	|- ( ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` 0 ) e. V )
8	6 7	syldan	|- ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. V )