This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )