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 ) ) )