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

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