Metamath Proof Explorer


Theorem wrdl2exs2

Description: A word of length two is a doubleton word. (Contributed by AV, 25-Jan-2021)

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

Proof

Step Hyp Ref Expression
1 1le2
 |-  1 <_ 2
2 breq2
 |-  ( ( # ` W ) = 2 -> ( 1 <_ ( # ` W ) <-> 1 <_ 2 ) )
3 1 2 mpbiri
 |-  ( ( # ` W ) = 2 -> 1 <_ ( # ` W ) )
4 wrdsymb1
 |-  ( ( W e. Word S /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. S )
5 3 4 sylan2
 |-  ( ( W e. Word S /\ ( # ` W ) = 2 ) -> ( W ` 0 ) e. S )
6 lsw
 |-  ( W e. Word S -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
7 oveq1
 |-  ( ( # ` W ) = 2 -> ( ( # ` W ) - 1 ) = ( 2 - 1 ) )
8 2m1e1
 |-  ( 2 - 1 ) = 1
9 7 8 eqtrdi
 |-  ( ( # ` W ) = 2 -> ( ( # ` W ) - 1 ) = 1 )
10 9 fveq2d
 |-  ( ( # ` W ) = 2 -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` 1 ) )
11 6 10 sylan9eq
 |-  ( ( W e. Word S /\ ( # ` W ) = 2 ) -> ( lastS ` W ) = ( W ` 1 ) )
12 2nn
 |-  2 e. NN
13 lswlgt0cl
 |-  ( ( 2 e. NN /\ ( W e. Word S /\ ( # ` W ) = 2 ) ) -> ( lastS ` W ) e. S )
14 12 13 mpan
 |-  ( ( W e. Word S /\ ( # ` W ) = 2 ) -> ( lastS ` W ) e. S )
15 11 14 eqeltrrd
 |-  ( ( W e. Word S /\ ( # ` W ) = 2 ) -> ( W ` 1 ) e. S )
16 wrdlen2s2
 |-  ( ( W e. Word S /\ ( # ` W ) = 2 ) -> W = <" ( W ` 0 ) ( W ` 1 ) "> )
17 id
 |-  ( s = ( W ` 0 ) -> s = ( W ` 0 ) )
18 eqidd
 |-  ( s = ( W ` 0 ) -> t = t )
19 17 18 s2eqd
 |-  ( s = ( W ` 0 ) -> <" s t "> = <" ( W ` 0 ) t "> )
20 19 eqeq2d
 |-  ( s = ( W ` 0 ) -> ( W = <" s t "> <-> W = <" ( W ` 0 ) t "> ) )
21 eqidd
 |-  ( t = ( W ` 1 ) -> ( W ` 0 ) = ( W ` 0 ) )
22 id
 |-  ( t = ( W ` 1 ) -> t = ( W ` 1 ) )
23 21 22 s2eqd
 |-  ( t = ( W ` 1 ) -> <" ( W ` 0 ) t "> = <" ( W ` 0 ) ( W ` 1 ) "> )
24 23 eqeq2d
 |-  ( t = ( W ` 1 ) -> ( W = <" ( W ` 0 ) t "> <-> W = <" ( W ` 0 ) ( W ` 1 ) "> ) )
25 20 24 rspc2ev
 |-  ( ( ( W ` 0 ) e. S /\ ( W ` 1 ) e. S /\ W = <" ( W ` 0 ) ( W ` 1 ) "> ) -> E. s e. S E. t e. S W = <" s t "> )
26 5 15 16 25 syl3anc
 |-  ( ( W e. Word S /\ ( # ` W ) = 2 ) -> E. s e. S E. t e. S W = <" s t "> )