P. 150 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14901-15000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	s5eqd 14901	Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅”⟩)
Theorem	s6eqd 14902	Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆”⟩)
Theorem	s7eqd 14903	Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    &   ⊢ (𝜑 → 𝐺 = 𝑇)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆𝑇”⟩)
Theorem	s8eqd 14904	Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    &   ⊢ (𝜑 → 𝐺 = 𝑇)    &   ⊢ (𝜑 → 𝐻 = 𝑈)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆𝑇𝑈”⟩)
Theorem	s3eq2 14905	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
⊢ (𝐵 = 𝐷 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐴𝐷𝐶”⟩)
Theorem	s2cld 14906	A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cld 14907	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s4cld 14908	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑋)
Theorem	s5cld 14909	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word 𝑋)
Theorem	s6cld 14910	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word 𝑋)
Theorem	s7cld 14911	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word 𝑋)
Theorem	s8cld 14912	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ Word 𝑋)
Theorem	s2cl 14913	A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cl 14914	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s2cli 14915	A doubleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵”⟩ ∈ Word V
Theorem	s3cli 14916	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ ∈ Word V
Theorem	s4cli 14917	A length 4 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word V
Theorem	s5cli 14918	A length 5 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word V
Theorem	s6cli 14919	A length 6 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word V
Theorem	s7cli 14920	A length 7 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word V
Theorem	s8cli 14921	A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ Word V
Theorem	s2fv0 14922	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 14923	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 14924	The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵”⟩) = 2
Theorem	s2dm 14925	The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.)
⊢ dom ⟨“𝐴𝐵”⟩ = {0, 1}
Theorem	s3fv0 14926	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘0) = 𝐴)
Theorem	s3fv1 14927	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘1) = 𝐵)
Theorem	s3fv2 14928	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘2) = 𝐶)
Theorem	s3len 14929	The length of a length 3 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶”⟩) = 3
Theorem	s4fv0 14930	Extract the first symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
Theorem	s4fv1 14931	Extract the second symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
Theorem	s4fv2 14932	Extract the third symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
Theorem	s4fv3 14933	Extract the fourth symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐷 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
Theorem	s4len 14934	The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷”⟩) = 4
Theorem	s5len 14935	The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸”⟩) = 5
Theorem	s6len 14936	The length of a length 6 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩) = 6
Theorem	s7len 14937	The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩) = 7
Theorem	s8len 14938	The length of a length 8 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩) = 8
Theorem	lsws2 14939	The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐵 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵”⟩) = 𝐵)
Theorem	lsws3 14940	The last symbol of a 3 letter word is its third symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐶 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵𝐶”⟩) = 𝐶)
Theorem	lsws4 14941	The last symbol of a 4 letter word is its fourth symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐷 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵𝐶𝐷”⟩) = 𝐷)
Theorem	s2prop 14942	A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ⟨“𝐴𝐵”⟩ = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩})
Theorem	s2dmALT 14943	Alternate version of s2dm 14925, 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 14944	A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ⟨“𝐴𝐵𝐶”⟩ = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩})
Theorem	s4prop 14945	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 14946	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 14947	The converse of a singleton word is a function. (Contributed by AV, 22-Jan-2021.)
⊢ Fun ◡⟨“𝐴”⟩
Theorem	funcnvs2 14948	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 14949	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 14950	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 14951	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 14952	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 14953	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 14954	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 14955	Mapping a doubleton word by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∘ ⟨“𝐴𝐵”⟩) = ⟨“(𝐹‘𝐴)(𝐹‘𝐵)”⟩)
Theorem	s3co 14956	Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∘ ⟨“𝐴𝐵𝐶”⟩) = ⟨“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”⟩)
Theorem	s0s1 14957	Concatenation of fixed length strings. (This special case of ccatlid 14620 is provided to complete the pattern s0s1 14957, df-s2 14883, df-s3 14884, ...) (Contributed by Mario Carneiro, 28-Feb-2016.)
⊢ ⟨“𝐴”⟩ = (∅ ++ ⟨“𝐴”⟩)
Theorem	s1s2 14958	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶”⟩)
Theorem	s1s3 14959	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷”⟩)
Theorem	s1s4 14960	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸”⟩)
Theorem	s1s5 14961	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹”⟩)
Theorem	s1s6 14962	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹𝐺”⟩)
Theorem	s1s7 14963	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩)
Theorem	s2s2 14964	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶𝐷”⟩)
Theorem	s4s2 14965	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹”⟩)
Theorem	s4s3 14966	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹𝐺”⟩)
Theorem	s4s4 14967	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹𝐺𝐻”⟩)
Theorem	s3s4 14968	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷𝐸𝐹𝐺”⟩)
Theorem	s2s5 14969	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶𝐷𝐸𝐹𝐺”⟩)
Theorem	s5s2 14970	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹𝐺”⟩)
Theorem	s2eq2s1eq 14971	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 14972	Two length 2 words are equal iff the corresponding symbols are equal. (Contributed by AV, 20-Oct-2018.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (⟨“𝐴𝐵”⟩ = ⟨“𝐶𝐷”⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	s3eqs2s1eq 14973	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 14974	Two length 3 words are equal iff the corresponding symbols are equal. (Contributed by AV, 4-Jan-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐷𝐸𝐹”⟩ ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹)))
Theorem	swrds2 14975	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	swrds2m 14976	Extract two adjacent symbols from a word in reverse direction. (Contributed by AV, 11-May-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (2...(♯‘𝑊))) → (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) = ⟨“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”⟩)
Theorem	wrdlen2i 14977	Implications of a word of length two. (Contributed by AV, 27-Jul-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇))))
Theorem	wrd2pr2op 14978	A word of length two 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 14979	A word of length two. (Contributed by AV, 20-Oct-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇))))
Theorem	wrdlen2s2 14980	A word of length two as doubleton word. (Contributed by AV, 20-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
Theorem	wrdl2exs2 14981*	A word of length two is a doubleton word. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 2) → ∃𝑠 ∈ 𝑆 ∃𝑡 ∈ 𝑆 𝑊 = ⟨“𝑠𝑡”⟩)
Theorem	pfx2 14982	A prefix of length two. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
Theorem	wrd3tpop 14983	A word of length three represented as triple of ordered pairs. (Contributed by AV, 26-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → 𝑊 = {⟨0, (𝑊‘0)⟩, ⟨1, (𝑊‘1)⟩, ⟨2, (𝑊‘2)⟩})
Theorem	wrdlen3s3 14984	A word of length three as length 3 string. (Contributed by AV, 26-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)(𝑊‘2)”⟩)
Theorem	repsw2 14985	The "repeated symbol word" of length two. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 2) = ⟨“𝑆𝑆”⟩)
Theorem	repsw3 14986	The "repeated symbol word" of length three. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 3) = ⟨“𝑆𝑆𝑆”⟩)
Theorem	swrd2lsw 14987	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 14988	Two words of length at least two 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 AV, 12-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑊 = 𝑈 ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈)))))
Theorem	ccatw2s1ccatws2 14989	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.) (Revised by AV, 29-Jan-2024.)
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) = (𝑊 ++ ⟨“𝑋𝑌”⟩))
Theorem	ccat2s1fvwALT 14990	Alternate proof of ccat2s1fvw 14672 using words of length 2, see df-s2 14883. 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.) (Revised by AV, 28-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (♯‘𝑊)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝐼) = (𝑊‘𝐼))
Theorem	wwlktovf 14991*	Lemma 1 for wrd2f1tovbij 14995. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷⟶𝑅
Theorem	wwlktovf1 14992*	Lemma 2 for wrd2f1tovbij 14995. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷–1-1→𝑅
Theorem	wwlktovfo 14993*	Lemma 3 for wrd2f1tovbij 14995. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–onto→𝑅)
Theorem	wwlktovf1o 14994*	Lemma 4 for wrd2f1tovbij 14995. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–1-1-onto→𝑅)
Theorem	wrd2f1tovbij 14995*	There is a bijection between words of length two with a fixed first symbol contained in a pair and the symbols contained in a pair together with the fixed symbol. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
⊢ ((𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉) → ∃𝑓 𝑓:{𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋})
Theorem	eqwrds3 14996	A word is equal with a length 3 string iff it has length 3 and the same symbol at each position. (Contributed by AV, 12-May-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = ⟨“𝐴𝐵𝐶”⟩ ↔ ((♯‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶))))
Theorem	wrdl3s3 14997*	A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
Theorem	s2rn 14998	Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof shortened by AV, 1-Aug-2025.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽”⟩ = {𝐼, 𝐽})
Theorem	s3rn 14999	Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof shortened by AV, 1-Aug-2025.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽𝐾”⟩ = {𝐼, 𝐽, 𝐾})
Theorem	s7rn 15000	Range of a length 7 string. (Contributed by AV, 30-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (({𝐴, 𝐵, 𝐶} ∪ {𝐷}) ∪ {𝐸, 𝐹, 𝐺}))