Metamath Proof Explorer

Theorem wrdlen1

Description: A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018) (Proof shortened by AV, 19-Oct-2018)

Ref Expression
Assertion wrdlen1 
|- ( ( W e. Word V /\ ( # ` W ) = 1 ) -> E. v e. V ( W ` 0 ) = v )

Proof

Step Hyp Ref Expression
1 1le1 
 |-  1 <_ 1
2 breq2 
 |-  ( ( # ` W ) = 1 -> ( 1 <_ ( # ` W ) <-> 1 <_ 1 ) )
3 1 2 mpbiri 
 |-  ( ( # ` W ) = 1 -> 1 <_ ( # ` W ) )
4 wrdsymb1 
 |-  ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. V )
5 3 4 sylan2 
 |-  ( ( W e. Word V /\ ( # ` W ) = 1 ) -> ( W ` 0 ) e. V )
6 clel5 
 |-  ( ( W ` 0 ) e. V <-> E. v e. V ( W ` 0 ) = v )
7 5 6 sylib 
 |-  ( ( W e. Word V /\ ( # ` W ) = 1 ) -> E. v e. V ( W ` 0 ) = v )