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