Metamath Proof Explorer

Theorem eqs1

Description: A word of length 1 is a singleton word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Proof shortened by AV, 1-May-2020)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( # ` W ) = 1 -> ( # ` W ) = 1 )
2 s1len 
 |-  ( # ` <" ( W ` 0 ) "> ) = 1
3 1 2 eqtr4di 
 |-  ( ( # ` W ) = 1 -> ( # ` W ) = ( # ` <" ( W ` 0 ) "> ) )
4 fvex 
 |-  ( W ` 0 ) e. _V
5 s1fv 
 |-  ( ( W ` 0 ) e. _V -> ( <" ( W ` 0 ) "> ` 0 ) = ( W ` 0 ) )
6 4 5 ax-mp 
 |-  ( <" ( W ` 0 ) "> ` 0 ) = ( W ` 0 )
7 6 eqcomi 
 |-  ( W ` 0 ) = ( <" ( W ` 0 ) "> ` 0 )
8 c0ex 
 |-  0 e. _V
9 fveq2 
 |-  ( x = 0 -> ( W ` x ) = ( W ` 0 ) )
10 fveq2 
 |-  ( x = 0 -> ( <" ( W ` 0 ) "> ` x ) = ( <" ( W ` 0 ) "> ` 0 ) )
11 9 10 eqeq12d 
 |-  ( x = 0 -> ( ( W ` x ) = ( <" ( W ` 0 ) "> ` x ) <-> ( W ` 0 ) = ( <" ( W ` 0 ) "> ` 0 ) ) )
12 8 11 ralsn 
 |-  ( A. x e. { 0 } ( W ` x ) = ( <" ( W ` 0 ) "> ` x ) <-> ( W ` 0 ) = ( <" ( W ` 0 ) "> ` 0 ) )
13 7 12 mpbir 
 |-  A. x e. { 0 } ( W ` x ) = ( <" ( W ` 0 ) "> ` x )
14 oveq2 
 |-  ( ( # ` W ) = 1 -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 1 ) )
15 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
16 14 15 eqtrdi 
 |-  ( ( # ` W ) = 1 -> ( 0 ..^ ( # ` W ) ) = { 0 } )
17 16 raleqdv 
 |-  ( ( # ` W ) = 1 -> ( A. x e. ( 0 ..^ ( # ` W ) ) ( W ` x ) = ( <" ( W ` 0 ) "> ` x ) <-> A. x e. { 0 } ( W ` x ) = ( <" ( W ` 0 ) "> ` x ) ) )
18 13 17 mpbiri 
 |-  ( ( # ` W ) = 1 -> A. x e. ( 0 ..^ ( # ` W ) ) ( W ` x ) = ( <" ( W ` 0 ) "> ` x ) )
19 3 18 jca 
 |-  ( ( # ` W ) = 1 -> ( ( # ` W ) = ( # ` <" ( W ` 0 ) "> ) /\ A. x e. ( 0 ..^ ( # ` W ) ) ( W ` x ) = ( <" ( W ` 0 ) "> ` x ) ) )
20 s1cli 
 |-  <" ( W ` 0 ) "> e. Word _V
21 eqwrd 
 |-  ( ( W e. Word A /\ <" ( W ` 0 ) "> e. Word _V ) -> ( W = <" ( W ` 0 ) "> <-> ( ( # ` W ) = ( # ` <" ( W ` 0 ) "> ) /\ A. x e. ( 0 ..^ ( # ` W ) ) ( W ` x ) = ( <" ( W ` 0 ) "> ` x ) ) ) )
22 20 21 mpan2 
 |-  ( W e. Word A -> ( W = <" ( W ` 0 ) "> <-> ( ( # ` W ) = ( # ` <" ( W ` 0 ) "> ) /\ A. x e. ( 0 ..^ ( # ` W ) ) ( W ` x ) = ( <" ( W ` 0 ) "> ` x ) ) ) )
23 19 22 syl5ibr 
 |-  ( W e. Word A -> ( ( # ` W ) = 1 -> W = <" ( W ` 0 ) "> ) )
24 23 imp 
 |-  ( ( W e. Word A /\ ( # ` W ) = 1 ) -> W = <" ( W ` 0 ) "> )