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

Metamath Proof Explorer

Theorem fstwrdne0

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

Ref Expression
Assertion fstwrdne0 
|- ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( W ` 0 ) e. V )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> W e. Word V )
2 nnge1 
 |-  ( N e. NN -> 1 <_ N )
3 2 adantr 
 |-  ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> 1 <_ N )
4 breq2 
 |-  ( ( # ` W ) = N -> ( 1 <_ ( # ` W ) <-> 1 <_ N ) )
5 4 ad2antll 
 |-  ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( 1 <_ ( # ` W ) <-> 1 <_ N ) )
6 3 5 mpbird 
 |-  ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> 1 <_ ( # ` W ) )
7 wrdsymb1 
 |-  ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. V )
8 1 6 7 syl2anc 
 |-  ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( W ` 0 ) e. V )