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.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ∘ 𝑆) = 𝑈)    &   ⊢ 𝑉 = (𝑈 ++ ⟨“(𝐹‘𝑋)”⟩)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝑇) = 𝑉)
Theorem	cats1cli 13602	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    ⇒   ⊢ 𝑇 ∈ Word V
Theorem	cats1fvn 13603	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    &   ⊢ (#‘𝑆) = 𝑀    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑇‘𝑀) = 𝑋)
Theorem	cats1fv 13604	A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    &   ⊢ (#‘𝑆) = 𝑀    &   ⊢ (𝑌 ∈ 𝑉 → (𝑆‘𝑁) = 𝑌)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑁 < 𝑀    ⇒   ⊢ (𝑌 ∈ 𝑉 → (𝑇‘𝑁) = 𝑌)
Theorem	cats1len 13605	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    &   ⊢ (#‘𝑆) = 𝑀    &   ⊢ (𝑀 + 1) = 𝑁    ⇒   ⊢ (#‘𝑇) = 𝑁
Theorem	cats1cat 13606	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐴 ∈ Word V    &   ⊢ 𝑆 ∈ Word V    &   ⊢ 𝐶 = (𝐵 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐵 = (𝐴 ++ 𝑆)    ⇒   ⊢ 𝐶 = (𝐴 ++ 𝑇)
Theorem	cats2cat 13607	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.)
⊢ 𝐵 ∈ Word V    &   ⊢ 𝐷 ∈ Word V    &   ⊢ 𝐴 = (𝐵 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐶 = (⟨“𝑌”⟩ ++ 𝐷)    ⇒   ⊢ (𝐴 ++ 𝐶) = ((𝐵 ++ ⟨“𝑋𝑌”⟩) ++ 𝐷)
Theorem	s2eqd 13608	Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
Theorem	s3eqd 13609	Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)
Theorem	s4eqd 13610	Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ = ⟨“𝑁𝑂𝑃𝑄”⟩)
Theorem	s5eqd 13611	Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅”⟩)
Theorem	s6eqd 13612	Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆”⟩)
Theorem	s7eqd 13613	Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    &   ⊢ (𝜑 → 𝐺 = 𝑇)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆𝑇”⟩)
Theorem	s8eqd 13614	Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    &   ⊢ (𝜑 → 𝐺 = 𝑇)    &   ⊢ (𝜑 → 𝐻 = 𝑈)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆𝑇𝑈”⟩)
Theorem	s3eq2 13615	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
⊢ (𝐵 = 𝐷 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐴𝐷𝐶”⟩)
Theorem	s2cld 13616	A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cld 13617	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s4cld 13618	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑋)
Theorem	s5cld 13619	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word 𝑋)
Theorem	s6cld 13620	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word 𝑋)
Theorem	s7cld 13621	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word 𝑋)
Theorem	s8cld 13622	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ Word 𝑋)
Theorem	s2cl 13623	A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cl 13624	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s2cli 13625	A doubleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵”⟩ ∈ Word V
Theorem	s3cli 13626	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ ∈ Word V
Theorem	s4cli 13627	A length 4 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word V
Theorem	s5cli 13628	A length 5 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word V
Theorem	s6cli 13629	A length 6 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word V
Theorem	s7cli 13630	A length 7 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word V
Theorem	s8cli 13631	A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ 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.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵”⟩‘0) = 𝐴)
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.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵”⟩‘1) = 𝐵)
Theorem	s2len 13634	The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (#‘⟨“𝐴𝐵”⟩) = 2
Theorem	s2dm 13635	The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.)
⊢ dom ⟨“𝐴𝐵”⟩ = {0, 1}
Theorem	s3fv0 13636	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘0) = 𝐴)
Theorem	s3fv1 13637	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘1) = 𝐵)
Theorem	s3fv2 13638	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘2) = 𝐶)
Theorem	s3len 13639	The length of a length 3 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (#‘⟨“𝐴𝐵𝐶”⟩) = 3
Theorem	s4fv0 13640	Extract the first symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
Theorem	s4fv1 13641	Extract the second symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
Theorem	s4fv2 13642	Extract the third symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
Theorem	s4fv3 13643	Extract the fourth symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐷 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
Theorem	s4len 13644	The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (#‘⟨“𝐴𝐵𝐶𝐷”⟩) = 4
Theorem	s5len 13645	The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (#‘⟨“𝐴𝐵𝐶𝐷𝐸”⟩) = 5
Theorem	s6len 13646	The length of a length 6 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (#‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩) = 6
Theorem	s7len 13647	The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (#‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩) = 7
Theorem	s8len 13648	The length of a length 8 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (#‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩) = 8
Theorem	lsws2 13649	The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐵 ∈ 𝑉 → ( lastS ‘⟨“𝐴𝐵”⟩) = 𝐵)
Theorem	lsws3 13650	The last symbol of a 3 letter word is its third symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐶 ∈ 𝑉 → ( lastS ‘⟨“𝐴𝐵𝐶”⟩) = 𝐶)
Theorem	lsws4 13651	The last symbol of a 4 letter word is its fourth symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐷 ∈ 𝑉 → ( lastS ‘⟨“𝐴𝐵𝐶𝐷”⟩) = 𝐷)
Theorem	s2prop 13652	A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ⟨“𝐴𝐵”⟩ = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩})
Theorem	s2dmALT 13653	Alternate version of s2dm 13635, having a shorter proof, but requiring that 𝐴 and 𝐵 are sets. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → dom ⟨“𝐴𝐵”⟩ = {0, 1})
Theorem	s3tpop 13654	A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ⟨“𝐴𝐵𝐶”⟩ = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩})
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.)
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ⟨“𝐴𝐵𝐶𝐷”⟩ = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐷⟩}))
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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ⟨“𝐴𝐵𝐶”⟩ Fn {0, 1, 2})
Theorem	funcnvs1 13657	The converse of a singleton word is a function. (Contributed by AV, 22-Jan-2021.)
⊢ Fun ◡⟨“𝐴”⟩
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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → Fun ◡⟨“𝐴𝐵”⟩)
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.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ◡⟨“𝐴𝐵𝐶”⟩)
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.)
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) → Fun ◡⟨“𝐴𝐵𝐶𝐷”⟩)
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.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐸 = ⟨“𝐴𝐵”⟩ → 𝐸:{0, 1}–1-1-onto→{𝐴, 𝐵}))
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.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐷⟩}):({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})))
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.)
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → (𝐸 = ⟨“𝐴𝐵𝐶𝐷”⟩ → 𝐸:dom 𝐸–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}))))
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.)
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐸 = ⟨“𝐴𝐵𝐶𝐷”⟩ → dom 𝐸 = ({0, 1} ∪ {2, 3})))
Theorem	s2co 13665	Mapping a doubleton word by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∘ ⟨“𝐴𝐵”⟩) = ⟨“(𝐹‘𝐴)(𝐹‘𝐵)”⟩)
Theorem	s3co 13666	Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∘ ⟨“𝐴𝐵𝐶”⟩) = ⟨“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”⟩)
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.)
⊢ ⟨“𝐴”⟩ = (∅ ++ ⟨“𝐴”⟩)
Theorem	s1s2 13668	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶”⟩)
Theorem	s1s3 13669	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷”⟩)
Theorem	s1s4 13670	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸”⟩)
Theorem	s1s5 13671	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹”⟩)
Theorem	s1s6 13672	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹𝐺”⟩)
Theorem	s1s7 13673	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩)
Theorem	s2s2 13674	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶𝐷”⟩)
Theorem	s4s2 13675	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹”⟩)
Theorem	s4s3 13676	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹𝐺”⟩)
Theorem	s4s4 13677	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹𝐺𝐻”⟩)
Theorem	s3s4 13678	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷𝐸𝐹𝐺”⟩)
Theorem	s2s5 13679	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶𝐷𝐸𝐹𝐺”⟩)
Theorem	s5s2 13680	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹𝐺”⟩)
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.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (⟨“𝐴𝐵”⟩ = ⟨“𝐶𝐷”⟩ ↔ (⟨“𝐴”⟩ = ⟨“𝐶”⟩ ∧ ⟨“𝐵”⟩ = ⟨“𝐷”⟩)))
Theorem	s2eq2seq 13682	Two length 2 words are equal iff the corresponding symbols are equal. (Contributed by AV, 20-Oct-2018.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (⟨“𝐴𝐵”⟩ = ⟨“𝐶𝐷”⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
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.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐷𝐸𝐹”⟩ ↔ (⟨“𝐴𝐵”⟩ = ⟨“𝐷𝐸”⟩ ∧ ⟨“𝐶”⟩ = ⟨“𝐹”⟩)))
Theorem	s3eq3seq 13684	Two length 3 words are equal iff the corresponding symbols are equal. (Contributed by AV, 4-Jan-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐷𝐸𝐹”⟩ ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹)))
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.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
Theorem	wrdlen2i 13686	Implications of a word of length 2. (Contributed by AV, 27-Jul-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇))))
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.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 2) → 𝑊 = {⟨0, (𝑊‘0)⟩, ⟨1, (𝑊‘1)⟩})
Theorem	wrdlen2 13688	A word of length 2. (Contributed by AV, 20-Oct-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} ↔ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇))))
Theorem	wrdlen2s2 13689	A word of length 2 as doubleton word. (Contributed by AV, 20-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 2) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
Theorem	wrdl2exs2 13690*	A word of length 2 is a doubleton word. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ (#‘𝑊) = 2) → ∃𝑠 ∈ 𝑆 ∃𝑡 ∈ 𝑆 𝑊 = ⟨“𝑠𝑡”⟩)
Theorem	wrd3tpop 13691	A word of length 3 represented as triple of ordered pairs. (Contributed by AV, 26-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → 𝑊 = {⟨0, (𝑊‘0)⟩, ⟨1, (𝑊‘1)⟩, ⟨2, (𝑊‘2)⟩})
Theorem	wrdlen3s3 13692	A word of length 3 as length 3 string. (Contributed by AV, 26-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)(𝑊‘2)”⟩)
Theorem	repsw2 13693	The "repeated symbol word" of length 2. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 2) = ⟨“𝑆𝑆”⟩)
Theorem	repsw3 13694	The "repeated symbol word" of length 3. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 3) = ⟨“𝑆𝑆𝑆”⟩)
Theorem	swrd2lsw 13695	Extract the last two symbols from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑊 substr ⟨((#‘𝑊) − 2), (#‘𝑊)⟩) = ⟨“(𝑊‘((#‘𝑊) − 2))( lastS ‘𝑊)”⟩)
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.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 substr ⟨0, ((#‘𝑊) − 2)⟩) = (𝑈 substr ⟨0, ((#‘𝑊) − 2)⟩) ∧ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈)))))
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.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) = (𝑊 ++ ⟨“𝑋𝑌”⟩))
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.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝐼) = (𝑊‘𝐼))
Theorem	wwlktovf 13699*	Lemma 1 for wrd2f1tovbij 13703. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷⟶𝑅
Theorem	wwlktovf1 13700*	Lemma 2 for wrd2f1tovbij 13703. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷–1-1→𝑅