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

Metamath Proof Explorer

Theorem wrdl1s1

Description: A word of length 1 is a singleton word consisting of the first symbol of the word. (Contributed by AV, 22-Jul-2018) (Proof shortened by AV, 14-Oct-2018)

Ref Expression
Assertion wrdl1s1 
|- ( S e. V -> ( W = <" S "> <-> ( W e. Word V /\ ( # ` W ) = 1 /\ ( W ` 0 ) = S ) ) )

Proof

Step Hyp Ref Expression
1 s1cl 
 |-  ( S e. V -> <" S "> e. Word V )
2 s1len 
 |-  ( # ` <" S "> ) = 1
3 2 a1i 
 |-  ( S e. V -> ( # ` <" S "> ) = 1 )
4 s1fv 
 |-  ( S e. V -> ( <" S "> ` 0 ) = S )
5 1 3 4 3jca 
 |-  ( S e. V -> ( <" S "> e. Word V /\ ( # ` <" S "> ) = 1 /\ ( <" S "> ` 0 ) = S ) )
6 eleq1 
 |-  ( W = <" S "> -> ( W e. Word V <-> <" S "> e. Word V ) )
7 fveqeq2 
 |-  ( W = <" S "> -> ( ( # ` W ) = 1 <-> ( # ` <" S "> ) = 1 ) )
8 fveq1 
 |-  ( W = <" S "> -> ( W ` 0 ) = ( <" S "> ` 0 ) )
9 8 eqeq1d 
 |-  ( W = <" S "> -> ( ( W ` 0 ) = S <-> ( <" S "> ` 0 ) = S ) )
10 6 7 9 3anbi123d 
 |-  ( W = <" S "> -> ( ( W e. Word V /\ ( # ` W ) = 1 /\ ( W ` 0 ) = S ) <-> ( <" S "> e. Word V /\ ( # ` <" S "> ) = 1 /\ ( <" S "> ` 0 ) = S ) ) )
11 5 10 syl5ibrcom 
 |-  ( S e. V -> ( W = <" S "> -> ( W e. Word V /\ ( # ` W ) = 1 /\ ( W ` 0 ) = S ) ) )
12 eqs1 
 |-  ( ( W e. Word V /\ ( # ` W ) = 1 ) -> W = <" ( W ` 0 ) "> )
13 s1eq 
 |-  ( ( W ` 0 ) = S -> <" ( W ` 0 ) "> = <" S "> )
14 13 eqeq2d 
 |-  ( ( W ` 0 ) = S -> ( W = <" ( W ` 0 ) "> <-> W = <" S "> ) )
15 12 14 syl5ibcom 
 |-  ( ( W e. Word V /\ ( # ` W ) = 1 ) -> ( ( W ` 0 ) = S -> W = <" S "> ) )
16 15 3impia 
 |-  ( ( W e. Word V /\ ( # ` W ) = 1 /\ ( W ` 0 ) = S ) -> W = <" S "> )
17 11 16 impbid1 
 |-  ( S e. V -> ( W = <" S "> <-> ( W e. Word V /\ ( # ` W ) = 1 /\ ( W ` 0 ) = S ) ) )