P. 151 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	s3eq2 15001	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
⊢ (𝐵 = 𝐷 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐴𝐷𝐶”⟩)
Theorem	s2cld 15002	A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cld 15003	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s4cld 15004	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑋)
Theorem	s5cld 15005	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word 𝑋)
Theorem	s6cld 15006	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word 𝑋)
Theorem	s7cld 15007	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word 𝑋)
Theorem	s8cld 15008	A length 8 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ Word 𝑋)
Theorem	s2cl 15009	A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cl 15010	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s2cli 15011	A doubleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵”⟩ ∈ Word V
Theorem	s3cli 15012	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ ∈ Word V
Theorem	s4cli 15013	A length 4 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word V
Theorem	s5cli 15014	A length 5 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word V
Theorem	s6cli 15015	A length 6 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word V
Theorem	s7cli 15016	A length 7 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word V
Theorem	s8cli 15017	A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ Word V
Theorem	s2fv0 15018	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 15019	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 15020	The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵”⟩) = 2
Theorem	s2dm 15021	The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.)
⊢ dom ⟨“𝐴𝐵”⟩ = {0, 1}
Theorem	s3fv0 15022	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘0) = 𝐴)
Theorem	s3fv1 15023	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘1) = 𝐵)
Theorem	s3fv2 15024	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘2) = 𝐶)
Theorem	s3len 15025	The length of a length 3 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶”⟩) = 3
Theorem	s4fv0 15026	Extract the first symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
Theorem	s4fv1 15027	Extract the second symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
Theorem	s4fv2 15028	Extract the third symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
Theorem	s4fv3 15029	Extract the fourth symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐷 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
Theorem	s4len 15030	The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷”⟩) = 4
Theorem	s5len 15031	The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸”⟩) = 5
Theorem	s6len 15032	The length of a length 6 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩) = 6
Theorem	s7len 15033	The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩) = 7
Theorem	s8len 15034	The length of a length 8 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩) = 8
Theorem	lsws2 15035	The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐵 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵”⟩) = 𝐵)
Theorem	lsws3 15036	The last symbol of a 3 letter word is its third symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐶 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵𝐶”⟩) = 𝐶)
Theorem	lsws4 15037	The last symbol of a 4 letter word is its fourth symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐷 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵𝐶𝐷”⟩) = 𝐷)
Theorem	s2prop 15038	A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ⟨“𝐴𝐵”⟩ = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩})
Theorem	s2dmALT 15039	Alternate version of s2dm 15021, 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 15040	A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ⟨“𝐴𝐵𝐶”⟩ = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩})
Theorem	s4prop 15041	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 15042	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 15043	The converse of a singleton word is a function. (Contributed by AV, 22-Jan-2021.)
⊢ Fun ◡⟨“𝐴”⟩
Theorem	funcnvs2 15044	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 15045	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 15046	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 15047	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 15048	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 15049	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 15050	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 15051	Mapping a doubleton word by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∘ ⟨“𝐴𝐵”⟩) = ⟨“(𝐹‘𝐴)(𝐹‘𝐵)”⟩)
Theorem	s3co 15052	Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∘ ⟨“𝐴𝐵𝐶”⟩) = ⟨“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”⟩)
Theorem	s0s1 15053	Concatenation of fixed length strings. (This special case of ccatlid 14712 is provided to complete the pattern s0s1 15053, df-s2 14979, df-s3 14980, ...) (Contributed by Mario Carneiro, 28-Feb-2016.)
⊢ ⟨“𝐴”⟩ = (∅ ++ ⟨“𝐴”⟩)
Theorem	s1s2 15054	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶”⟩)
Theorem	s1s3 15055	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷”⟩)
Theorem	s1s4 15056	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸”⟩)
Theorem	s1s5 15057	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹”⟩)
Theorem	s1s6 15058	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹𝐺”⟩)
Theorem	s1s7 15059	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩)
Theorem	s2s2 15060	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶𝐷”⟩)
Theorem	s4s2 15061	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹”⟩)
Theorem	s4s3 15062	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹𝐺”⟩)
Theorem	s4s4 15063	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸𝐹𝐺𝐻”⟩)
Theorem	s3s4 15064	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷𝐸𝐹𝐺”⟩)
Theorem	s2s5 15065	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶𝐷𝐸𝐹𝐺”⟩)
Theorem	s5s2 15066	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹𝐺”⟩)
Theorem	s2eq2s1eq 15067	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 15068	Two length 2 words are equal iff the corresponding symbols are equal. (Contributed by AV, 20-Oct-2018.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (⟨“𝐴𝐵”⟩ = ⟨“𝐶𝐷”⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	s3eqs2s1eq 15069	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 15070	Two length 3 words are equal iff the corresponding symbols are equal. (Contributed by AV, 4-Jan-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐷 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉)) → (⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐷𝐸𝐹”⟩ ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹)))
Theorem	swrds2 15071	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 15072	Extract two adjacent symbols from a word in reverse direction. (Contributed by AV, 11-May-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (2...(♯‘𝑊))) → (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) = ⟨“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”⟩)
Theorem	wrdlen2i 15073	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 15074	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 15075	A word of length two. (Contributed by AV, 20-Oct-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇))))
Theorem	wrdlen2s2 15076	A word of length two as doubleton word. (Contributed by AV, 20-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
Theorem	wrdl2exs2 15077*	A word of length two is a doubleton word. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 2) → ∃𝑠 ∈ 𝑆 ∃𝑡 ∈ 𝑆 𝑊 = ⟨“𝑠𝑡”⟩)
Theorem	pfx2 15078	A prefix of length two. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
Theorem	wrd3tpop 15079	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 15080	A word of length three as length 3 string. (Contributed by AV, 26-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) → 𝑊 = ⟨“(𝑊‘0)(𝑊‘1)(𝑊‘2)”⟩)
Theorem	s3rex 15081*	Membership in a family of words of length 3. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑆 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝑆 ↑m (0..^3)) ↔ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑆 𝐴 = ⟨“𝑥𝑦𝑧”⟩)
Theorem	s3rexrd 15082	Converse of s3rex 15081, deduction form. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∈ (𝑆 ↑m (0..^3)))
Theorem	repsw2 15083	The "repeated symbol word" of length two. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 2) = ⟨“𝑆𝑆”⟩)
Theorem	repsw3 15084	The "repeated symbol word" of length three. (Contributed by AV, 6-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 3) = ⟨“𝑆𝑆𝑆”⟩)
Theorem	swrd2lsw 15085	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 15086	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 15087	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 15088	Alternate proof of ccat2s1fvw 14766 using words of length 2, see df-s2 14979. 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 15089*	Lemma 1 for wrd2f1tovbij 15093. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷⟶𝑅
Theorem	wwlktovf1 15090*	Lemma 2 for wrd2f1tovbij 15093. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ 𝐹:𝐷–1-1→𝑅
Theorem	wwlktovfo 15091*	Lemma 3 for wrd2f1tovbij 15093. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–onto→𝑅)
Theorem	wwlktovf1o 15092*	Lemma 4 for wrd2f1tovbij 15093. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1))    ⇒   ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–1-1-onto→𝑅)
Theorem	wrd2f1tovbij 15093*	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 15094	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 15095*	A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
Theorem	s2rn 15096	Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof shortened by AV, 1-Aug-2025.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽”⟩ = {𝐼, 𝐽})
Theorem	s3rn 15097	Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof shortened by AV, 1-Aug-2025.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽𝐾”⟩ = {𝐼, 𝐽, 𝐾})
Theorem	s7rn 15098	Range of a length 7 string. (Contributed by AV, 30-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (({𝐴, 𝐵, 𝐶} ∪ {𝐷}) ∪ {𝐸, 𝐹, 𝐺}))
Theorem	s7f1o 15099	A length 7 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by AV, 2-Aug-2025.)
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐷 ∈ 𝑉 ∧ (𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉)) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺)) ∧ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ (𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺)) ∧ (𝐶 ≠ 𝐷 ∧ (𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺))) ∧ ((𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺) ∧ (𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺)))) → (𝐾 = ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ → 𝐾:(0..^7)–1-1-onto→(({𝐴, 𝐵, 𝐶} ∪ {𝐷}) ∪ {𝐸, 𝐹, 𝐺})))
Theorem	s3sndisj 15100*	The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑍 {⟨“𝐴𝐵𝑐”⟩})