Metamath Proof Explorer

Theorem wrdl1exs1

Description: A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021)

Ref Expression
Assertion wrdl1exs1 
|- ( ( W e. Word S /\ ( # ` W ) = 1 ) -> E. s e. S W = <" s "> )

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 S /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. S )
5 3 4 sylan2 
 |-  ( ( W e. Word S /\ ( # ` W ) = 1 ) -> ( W ` 0 ) e. S )
6 s1eq 
 |-  ( s = ( W ` 0 ) -> <" s "> = <" ( W ` 0 ) "> )
7 6 adantl 
 |-  ( ( ( W e. Word S /\ ( # ` W ) = 1 ) /\ s = ( W ` 0 ) ) -> <" s "> = <" ( W ` 0 ) "> )
8 7 eqeq2d 
 |-  ( ( ( W e. Word S /\ ( # ` W ) = 1 ) /\ s = ( W ` 0 ) ) -> ( W = <" s "> <-> W = <" ( W ` 0 ) "> ) )
9 eqs1 
 |-  ( ( W e. Word S /\ ( # ` W ) = 1 ) -> W = <" ( W ` 0 ) "> )
10 5 8 9 rspcedvd 
 |-  ( ( W e. Word S /\ ( # ` W ) = 1 ) -> E. s e. S W = <" s "> )