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