P. 137 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13601-13700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cats1co 13601	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word A )   &    |- ( ph -> X e. A )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ( F o. S ) = U )   &    |- V = ( U ++ <" ( F ` X ) "> )   =>    |- ( ph -> ( F o. T ) = V )
Theorem	cats1cli 13602	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- S e. Word _V   =>    |- T e. Word _V
Theorem	cats1fvn 13603	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- S e. Word _V   &    |- ( # ` S ) = M   =>    |- ( X e. V -> ( T ` M ) = X )
Theorem	cats1fv 13604	A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- S e. Word _V   &    |- ( # ` S ) = M   &    |- ( Y e. V -> ( S ` N ) = Y )   &    |- N e. NN0   &    |- N < M   =>    |- ( Y e. V -> ( T ` N ) = Y )
Theorem	cats1len 13605	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- S e. Word _V   &    |- ( # ` S ) = M   &    |- ( M + 1 ) = N   =>    |- ( # ` T ) = N
Theorem	cats1cat 13606	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- A e. Word _V   &    |- S e. Word _V   &    |- C = ( B ++ <" X "> )   &    |- B = ( A ++ S )   =>    |- C = ( A ++ T )
Theorem	cats2cat 13607	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.)
|- B e. Word _V   &    |- D e. Word _V   &    |- A = ( B ++ <" X "> )   &    |- C = ( <" Y "> ++ D )   =>    |- ( A ++ C ) = ( ( B ++ <" X Y "> ) ++ D )
Theorem	s2eqd 13608	Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   =>    |- ( ph -> <" A B "> = <" N O "> )
Theorem	s3eqd 13609	Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   =>    |- ( ph -> <" A B C "> = <" N O P "> )
Theorem	s4eqd 13610	Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   =>    |- ( ph -> <" A B C D "> = <" N O P Q "> )
Theorem	s5eqd 13611	Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   =>    |- ( ph -> <" A B C D E "> = <" N O P Q R "> )
Theorem	s6eqd 13612	Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   =>    |- ( ph -> <" A B C D E F "> = <" N O P Q R S "> )
Theorem	s7eqd 13613	Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   &    |- ( ph -> G = T )   =>    |- ( ph -> <" A B C D E F G "> = <" N O P Q R S T "> )
Theorem	s8eqd 13614	Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   &    |- ( ph -> G = T )   &    |- ( ph -> H = U )   =>    |- ( ph -> <" A B C D E F G H "> = <" N O P Q R S T U "> )
Theorem	s3eq2 13615	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
|- ( B = D -> <" A B C "> = <" A D C "> )
Theorem	s2cld 13616	A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> <" A B "> e. Word X )
Theorem	s3cld 13617	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   =>    |- ( ph -> <" A B C "> e. Word X )
Theorem	s4cld 13618	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   =>    |- ( ph -> <" A B C D "> e. Word X )
Theorem	s5cld 13619	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   =>    |- ( ph -> <" A B C D E "> e. Word X )
Theorem	s6cld 13620	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   =>    |- ( ph -> <" A B C D E F "> e. Word X )
Theorem	s7cld 13621	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   =>    |- ( ph -> <" A B C D E F G "> e. Word X )
Theorem	s8cld 13622	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   &    |- ( ph -> H e. X )   =>    |- ( ph -> <" A B C D E F G H "> e. Word X )
Theorem	s2cl 13623	A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. X /\ B e. X ) -> <" A B "> e. Word X )
Theorem	s3cl 13624	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. X /\ B e. X /\ C e. X ) -> <" A B C "> e. Word X )
Theorem	s2cli 13625	A doubleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B "> e. Word _V
Theorem	s3cli 13626	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C "> e. Word _V
Theorem	s4cli 13627	A length 4 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> e. Word _V
Theorem	s5cli 13628	A length 5 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E "> e. Word _V
Theorem	s6cli 13629	A length 6 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F "> e. Word _V
Theorem	s7cli 13630	A length 7 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G "> e. Word _V
Theorem	s8cli 13631	A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G H "> e. Word _V
Theorem	s2fv0 13632	Extract the first symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( A e. V -> ( <" A B "> ` 0 ) = A )
Theorem	s2fv1 13633	Extract the second symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( B e. V -> ( <" A B "> ` 1 ) = B )
Theorem	s2len 13634	The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B "> ) = 2
Theorem	s2dm 13635	The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.)
|- dom <" A B "> = { 0 , 1 }
Theorem	s3fv0 13636	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( A e. V -> ( <" A B C "> ` 0 ) = A )
Theorem	s3fv1 13637	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( B e. V -> ( <" A B C "> ` 1 ) = B )
Theorem	s3fv2 13638	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( C e. V -> ( <" A B C "> ` 2 ) = C )
Theorem	s3len 13639	The length of a length 3 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C "> ) = 3
Theorem	s4fv0 13640	Extract the first symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
|- ( A e. V -> ( <" A B C D "> ` 0 ) = A )
Theorem	s4fv1 13641	Extract the second symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
|- ( B e. V -> ( <" A B C D "> ` 1 ) = B )
Theorem	s4fv2 13642	Extract the third symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
|- ( C e. V -> ( <" A B C D "> ` 2 ) = C )
Theorem	s4fv3 13643	Extract the fourth symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
|- ( D e. V -> ( <" A B C D "> ` 3 ) = D )
Theorem	s4len 13644	The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D "> ) = 4
Theorem	s5len 13645	The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D E "> ) = 5
Theorem	s6len 13646	The length of a length 6 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D E F "> ) = 6
Theorem	s7len 13647	The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D E F G "> ) = 7
Theorem	s8len 13648	The length of a length 8 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D E F G H "> ) = 8
Theorem	lsws2 13649	The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021.)
|- ( B e. V -> ( lastS ` <" A B "> ) = B )
Theorem	lsws3 13650	The last symbol of a 3 letter word is its third symbol. (Contributed by AV, 8-Feb-2021.)
|- ( C e. V -> ( lastS ` <" A B C "> ) = C )
Theorem	lsws4 13651	The last symbol of a 4 letter word is its fourth symbol. (Contributed by AV, 8-Feb-2021.)
|- ( D e. V -> ( lastS ` <" A B C D "> ) = D )
Theorem	s2prop 13652	A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
|- ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
Theorem	s2dmALT 13653	Alternate version of s2dm 13635, having a shorter proof, but requiring that A and B are sets. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. S /\ B e. S ) -> dom <" A B "> = { 0 , 1 } )
Theorem	s3tpop 13654	A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021.)
|- ( ( A e. S /\ B e. S /\ C e. S ) -> <" A B C "> = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )
Theorem	s4prop 13655	A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B C D "> = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) )
Theorem	s3fn 13656	A length 3 word is a function with a triple as domain. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by AV, 23-Jan-2021.)
|- ( ( A e. V /\ B e. V /\ C e. V ) -> <" A B C "> Fn { 0 , 1 , 2 } )
Theorem	funcnvs1 13657	The converse of a singleton word is a function. (Contributed by AV, 22-Jan-2021.)
|- Fun `' <" A ">
Theorem	funcnvs2 13658	The converse of a length 2 word is a function if its symbols are different sets. (Contributed by AV, 23-Jan-2021.)
|- ( ( A e. V /\ B e. V /\ A =/= B ) -> Fun `' <" A B "> )
Theorem	funcnvs3 13659	The converse of a length 3 word is a function if its symbols are different sets. (Contributed by Alexander van der Vekens, 31-Jan-2018.) (Revised by AV, 23-Jan-2021.)
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> Fun `' <" A B C "> )
Theorem	funcnvs4 13660	The converse of a length 4 word is a function if its symbols are different sets. (Contributed by AV, 10-Feb-2021.)
|- ( ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> Fun `' <" A B C D "> )
Theorem	s2f1o 13661	A length 2 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
|- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( E = <" A B "> -> E : { 0 , 1 } -1-1-onto-> { A , B } ) )
Theorem	f1oun2prg 13662	A union of unordered pairs of ordered pairs with different elements is a one-to-one onto function. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) )
Theorem	s4f1o 13663	A length 4 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( E = <" A B C D "> -> E : dom E -1-1-onto-> ( { A , B } u. { C , D } ) ) ) )
Theorem	s4dom 13664	The domain of a length 4 word is the union of two (disjunct) pairs. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( E = <" A B C D "> -> dom E = ( { 0 , 1 } u. { 2 , 3 } ) ) )
Theorem	s2co 13665	Mapping a doubleton word by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> F : X --> Y )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> ( F o. <" A B "> ) = <" ( F ` A ) ( F ` B ) "> )
Theorem	s3co 13666	Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> F : X --> Y )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   =>    |- ( ph -> ( F o. <" A B C "> ) = <" ( F ` A ) ( F ` B ) ( F ` C ) "> )
Theorem	s0s1 13667	Concatenation of fixed length strings. (This special case of ccatlid 13369 is provided to complete the pattern s0s1 13667, df-s2 13593, df-s3 13594, ...) (Contributed by Mario Carneiro, 28-Feb-2016.)
|- <" A "> = ( (/) ++ <" A "> )
Theorem	s1s2 13668	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C "> = ( <" A "> ++ <" B C "> )
Theorem	s1s3 13669	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> = ( <" A "> ++ <" B C D "> )
Theorem	s1s4 13670	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E "> = ( <" A "> ++ <" B C D E "> )
Theorem	s1s5 13671	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F "> = ( <" A "> ++ <" B C D E F "> )
Theorem	s1s6 13672	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G "> = ( <" A "> ++ <" B C D E F G "> )
Theorem	s1s7 13673	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G H "> = ( <" A "> ++ <" B C D E F G H "> )
Theorem	s2s2 13674	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> = ( <" A B "> ++ <" C D "> )
Theorem	s4s2 13675	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F "> = ( <" A B C D "> ++ <" E F "> )
Theorem	s4s3 13676	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> )
Theorem	s4s4 13677	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G H "> = ( <" A B C D "> ++ <" E F G H "> )
Theorem	s3s4 13678	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- <" A B C D E F G "> = ( <" A B C "> ++ <" D E F G "> )
Theorem	s2s5 13679	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- <" A B C D E F G "> = ( <" A B "> ++ <" C D E F G "> )
Theorem	s5s2 13680	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- <" A B C D E F G "> = ( <" A B C D E "> ++ <" F G "> )
Theorem	s2eq2s1eq 13681	Two length 2 words are equal iff the corresponding singleton words consisting of their symbols are equal. (Contributed by Alexander van der Vekens, 24-Sep-2018.)
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( <" A "> = <" C "> /\ <" B "> = <" D "> ) ) )
Theorem	s2eq2seq 13682	Two length 2 words are equal iff the corresponding symbols are equal. (Contributed by AV, 20-Oct-2018.)
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( A = C /\ B = D ) ) )
Theorem	s3eqs2s1eq 13683	Two length 3 words are equal iff the corresponding length 2 words and singleton words consisting of their symbols are equal. (Contributed by AV, 4-Jan-2022.)
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B C "> = <" D E F "> <-> ( <" A B "> = <" D E "> /\ <" C "> = <" F "> ) ) )
Theorem	s3eq3seq 13684	Two length 3 words are equal iff the corresponding symbols are equal. (Contributed by AV, 4-Jan-2022.)
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B C "> = <" D E F "> <-> ( A = D /\ B = E /\ C = F ) ) )
Theorem	swrds2 13685	Extract two adjacent symbols from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( W e. Word A /\ I e. NN0 /\ ( I + 1 ) e. ( 0..^ ( # ` W ) ) ) -> ( W substr <. I , ( I + 2 ) >. ) = <" ( W ` I ) ( W ` ( I + 1 ) ) "> )
Theorem	wrdlen2i 13686	Implications of a word of length 2. (Contributed by AV, 27-Jul-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( S e. V /\ T e. V ) -> ( W = { <. 0 , S >. , <. 1 , T >. } -> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) ) )
Theorem	wrd2pr2op 13687	A word of length 2 represented as unordered pair of ordered pairs. (Contributed by AV, 20-Oct-2018.) (Proof shortened by AV, 26-Jan-2021.)
|- ( ( W e. Word V /\ ( # ` W ) = 2 ) -> W = { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. } )
Theorem	wrdlen2 13688	A word of length 2. (Contributed by AV, 20-Oct-2018.)
|- ( ( S e. V /\ T e. V ) -> ( W = { <. 0 , S >. , <. 1 , T >. } <-> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) ) )
Theorem	wrdlen2s2 13689	A word of length 2 as doubleton word. (Contributed by AV, 20-Oct-2018.)
|- ( ( W e. Word V /\ ( # ` W ) = 2 ) -> W = <" ( W ` 0 ) ( W ` 1 ) "> )
Theorem	wrdl2exs2 13690*	A word of length 2 is a doubleton word. (Contributed by AV, 25-Jan-2021.)
|- ( ( W e. Word S /\ ( # ` W ) = 2 ) -> E. s e. S E. t e. S W = <" s t "> )
Theorem	wrd3tpop 13691	A word of length 3 represented as triple of ordered pairs. (Contributed by AV, 26-Jan-2021.)
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) -> W = { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. , <. 2 , ( W ` 2 ) >. } )
Theorem	wrdlen3s3 13692	A word of length 3 as length 3 string. (Contributed by AV, 26-Jan-2021.)
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) -> W = <" ( W ` 0 ) ( W ` 1 ) ( W ` 2 ) "> )
Theorem	repsw2 13693	The "repeated symbol word" of length 2. (Contributed by AV, 6-Nov-2018.)
|- ( S e. V -> ( S repeatS 2 ) = <" S S "> )
Theorem	repsw3 13694	The "repeated symbol word" of length 3. (Contributed by AV, 6-Nov-2018.)
|- ( S e. V -> ( S repeatS 3 ) = <" S S S "> )
Theorem	swrd2lsw 13695	Extract the last two symbols from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
|- ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> )
Theorem	2swrd2eqwrdeq 13696	Two words of length at least 2 are equal if and only if they have the same prefix and the same two single symbols suffix. (Contributed by AV, 24-Sep-2018.) (Revised by Mario Carneiro/AV, 23-Oct-2018.)
|- ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W substr <. 0 , ( ( # ` W ) - 2 ) >. ) = ( U substr <. 0 , ( ( # ` W ) - 2 ) >. ) /\ ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
Theorem	ccatw2s1ccatws2 13697	The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton word consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018.)
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ <" X Y "> ) )
Theorem	ccat2s1fvwALT 13698	Alternate proof of ccat2s1fvw 13415 using words of length 2, see df-s2 13593. A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018.) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )
Theorem	wwlktovf 13699*	Lemma 1 for wrd2f1tovbij 13703. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- F : D --> R
Theorem	wwlktovf1 13700*	Lemma 2 for wrd2f1tovbij 13703. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- F : D -1-1-> R