P. 146 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14501-14600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wrd0 14501	The empty set is a word (the empty word, frequently denoted ε in this context). This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 13-May-2020.)
⊢ ∅ ∈ Word 𝑆
Theorem	0wrd0 14502	The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)
⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅)
Theorem	ffz0iswrd 14503	A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.) (Proof shortened by JJ, 18-Nov-2022.)
⊢ (𝑊:(0...𝐿)⟶𝑆 → 𝑊 ∈ Word 𝑆)
Theorem	wrdsymb 14504	A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.)
⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆))))
Theorem	nfwrd 14505	Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ Ⅎ𝑥𝑆    ⇒   ⊢ Ⅎ𝑥Word 𝑆
Theorem	csbwrdg 14506*	Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆)
Theorem	wrdnval 14507*	Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Proof shortened by AV, 13-May-2020.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁} = (𝑉 ↑m (0..^𝑁)))
Theorem	wrdmap 14508	Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑m (0..^𝑁))))
Theorem	hashwrdn 14509*	If there is only a finite number of symbols, the number of words of a fixed length over these sysmbols is the number of these symbols raised to the power of the length. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
⊢ ((𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0) → (♯‘{𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁}) = ((♯‘𝑉)↑𝑁))
Theorem	wrdnfi 14510*	If there is only a finite number of symbols, the number of words of a fixed length over these symbols is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018.) Remove unnecessary antecedent. (Revised by JJ, 18-Nov-2022.)
⊢ (𝑉 ∈ Fin → {𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁} ∈ Fin)
Theorem	wrdsymb0 14511	A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018.) (Proof shortened by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐼 < 0 ∨ (♯‘𝑊) ≤ 𝐼) → (𝑊‘𝐼) = ∅))
Theorem	wrdlenge1n0 14512	A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊)))
Theorem	len0nnbi 14513	The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ))
Theorem	wrdlenge2n0 14514	A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 𝑊 ≠ ∅)
Theorem	wrdsymb1 14515	The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑊)) → (𝑊‘0) ∈ 𝑉)
Theorem	wrdlen1 14516*	A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018.) (Proof shortened by AV, 19-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 1) → ∃𝑣 ∈ 𝑉 (𝑊‘0) = 𝑣)
Theorem	fstwrdne 14517	The first symbol of a nonempty word is an element of the alphabet for the word. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉)
Theorem	fstwrdne0 14518	The first symbol of a nonempty word is an element of the alphabet for the word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)) → (𝑊‘0) ∈ 𝑉)
Theorem	eqwrd 14519*	Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) (Revised by JJ, 30-Dec-2023.)
⊢ ((𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇) → (𝑈 = 𝑊 ↔ ((♯‘𝑈) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑈))(𝑈‘𝑖) = (𝑊‘𝑖))))
Theorem	elovmpowrd 14520*	Implications for the value of an operation defined by the maps-to notation with a class abstraction of words as a result having an element. Note that 𝜑 may depend on 𝑧 as well as on 𝑣 and 𝑦. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ 𝑂 = (𝑣 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ Word 𝑣 ∣ 𝜑})    ⇒   ⊢ (𝑍 ∈ (𝑉𝑂𝑌) → (𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉))
Theorem	elovmptnn0wrd 14521*	Implications for the value of an operation defined by the maps-to notation with a function of nonnegative integers into a class abstraction of words as a result having an element. Note that 𝜑 may depend on 𝑧 as well as on 𝑣 and 𝑦 and 𝑛. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.)
⊢ 𝑂 = (𝑣 ∈ V, 𝑦 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑧 ∈ Word 𝑣 ∣ 𝜑}))    ⇒   ⊢ (𝑍 ∈ ((𝑉𝑂𝑌)‘𝑁) → ((𝑉 ∈ V ∧ 𝑌 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ Word 𝑉)))
Theorem	wrdred1 14522	A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)
⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆)
Theorem	wrdred1hash 14523	The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (♯‘𝐹)) → (♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))) = ((♯‘𝐹) − 1))
5.7.2  Last symbol of a word
Syntax	clsw 14524	Extend class notation with the Last Symbol of a word.
class lastS
Definition	df-lsw 14525	Extract the last symbol of a word. May be not meaningful for other sets which are not words. The name lastS (as abbreviation of "lastSymbol") is a compromise between usually used names for corresponding functions in computer programs (as last() or lastChar()), the terminology used for words in set.mm ("symbol" instead of "character") and brevity ("lastS" is shorter than "lastChar" and "lastSymbol"). Labels of theorems about last symbols of a word will contain the abbreviation "lsw" (Last Symbol of a Word). (Contributed by Alexander van der Vekens, 18-Mar-2018.)
⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
Theorem	lsw 14526	Extract the last symbol of a word. May be not meaningful for other sets which are not words. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
Theorem	lsw0 14527	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 19-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 0) → (lastS‘𝑊) = ∅)
Theorem	lsw0g 14528	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)
⊢ (lastS‘∅) = ∅
Theorem	lsw1 14529	The last symbol of a word of length 1 is the first symbol of this word. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 1) → (lastS‘𝑊) = (𝑊‘0))
Theorem	lswcl 14530	Closure of the last symbol: the last symbol of a nonempty word belongs to the alphabet for the word. (Contributed by AV, 2-Aug-2018.) (Proof shortened by AV, 29-Apr-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (lastS‘𝑊) ∈ 𝑉)
Theorem	lswlgt0cl 14531	The last symbol of a nonempty word is an element of the alphabet for the word. (Contributed by Alexander van der Vekens, 1-Oct-2018.) (Proof shortened by AV, 29-Apr-2020.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)) → (lastS‘𝑊) ∈ 𝑉)
5.7.3  Concatenations of words
Syntax	cconcat 14532	Syntax for the concatenation operator.
class ++
Definition	df-concat 14533*	Define the concatenation operator which combines two words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 15-Aug-2015.)
⊢ ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))
Theorem	ccatfn 14534	The concatenation operator is a two-argument function. (Contributed by Mario Carneiro, 27-Sep-2015.) (Proof shortened by AV, 29-Apr-2020.)
⊢ ++ Fn (V × V)
Theorem	ccatfval 14535*	Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))))
Theorem	ccatcl 14536	The concatenation of two words is a word. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 29-Apr-2020.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵)
Theorem	ccatlen 14537	The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇)))
Theorem	ccat0 14538	The concatenation of two words is empty iff the two words are empty. (Contributed by AV, 4-Mar-2022.) (Revised by JJ, 18-Jan-2024.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) = ∅ ↔ (𝑆 = ∅ ∧ 𝑇 = ∅)))
Theorem	ccatval1 14539	Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 30-Apr-2020.) (Revised by JJ, 18-Jan-2024.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝐼) = (𝑆‘𝐼))
Theorem	ccatval2 14540	Value of a symbol in the right half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝐼) = (𝑇‘(𝐼 − (♯‘𝑆))))
Theorem	ccatval3 14541	Value of a symbol in the right half of a concatenated word, using an index relative to the subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof shortened by AV, 30-Apr-2020.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝐼 + (♯‘𝑆))) = (𝑇‘𝐼))
Theorem	elfzelfzccat 14542	An element of a finite set of sequential integers up to the length of a word is an element of an extended finite set of sequential integers up to the length of a concatenation of this word with another word. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(♯‘𝐴)) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))))
Theorem	ccatvalfn 14543	The concatenation of two words is a function over the half-open integer range having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) Fn (0..^((♯‘𝐴) + (♯‘𝐵))))
Theorem	ccatdmss 14544	The domain of a concatenated word is a superset of the domain of the first word. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐴 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → dom 𝐴 ⊆ dom (𝐴 ++ 𝐵))
Theorem	ccatsymb 14545	The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018.) (Proof shortened by AV, 24-Nov-2018.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵)‘𝐼) = if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴)))))
Theorem	ccatfv0 14546	The first symbol of a concatenation of two words is the first symbol of the first word if the first word is not empty. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 < (♯‘𝐴)) → ((𝐴 ++ 𝐵)‘0) = (𝐴‘0))
Theorem	ccatval1lsw 14547	The last symbol of the left (nonempty) half of a concatenated word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴))
Theorem	ccatval21sw 14548	The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0))
Theorem	ccatlid 14549	Concatenation of a word by the empty word on the left. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
⊢ (𝑆 ∈ Word 𝐵 → (∅ ++ 𝑆) = 𝑆)
Theorem	ccatrid 14550	Concatenation of a word by the empty word on the right. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
⊢ (𝑆 ∈ Word 𝐵 → (𝑆 ++ ∅) = 𝑆)
Theorem	ccatass 14551	Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈)))
Theorem	ccatrn 14552	The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇))
Theorem	ccatidid 14553	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
⊢ (∅ ++ ∅) = ∅
Theorem	lswccatn0lsw 14554	The last symbol of a word concatenated with a nonempty word is the last symbol of the nonempty word. (Contributed by AV, 22-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (lastS‘(𝐴 ++ 𝐵)) = (lastS‘𝐵))
Theorem	lswccat0lsw 14555	The last symbol of a word concatenated with the empty word is the last symbol of the word. (Contributed by AV, 22-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ (𝑊 ∈ Word 𝑉 → (lastS‘(𝑊 ++ ∅)) = (lastS‘𝑊))
Theorem	ccatalpha 14556	A concatenation of two arbitrary words is a word over an alphabet iff the symbols of both words belong to the alphabet. (Contributed by AV, 28-Feb-2021.)
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))
Theorem	ccatrcl1 14557	Reverse closure of a concatenation: If the concatenation of two arbitrary words is a word over an alphabet then the symbols of the first word belong to the alphabet. (Contributed by AV, 3-Mar-2021.)
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (𝑊 = (𝐴 ++ 𝐵) ∧ 𝑊 ∈ Word 𝑆)) → 𝐴 ∈ Word 𝑆)
5.7.4  Singleton words
Syntax	cs1 14558	Syntax for the singleton word constructor.
class ⟨“𝐴”⟩
Definition	df-s1 14559	Define the canonical injection from symbols to words. Although not required, 𝐴 should usually be a set. Otherwise, the singleton word ⟨“𝐴”⟩ would be the singleton word consisting of the empty set, see s1prc 14567, and not, as maybe expected, the empty word, see also s1nz 14570. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Theorem	ids1 14560	Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ = ⟨“( I ‘𝐴)”⟩
Theorem	s1val 14561	Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝑉 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
Theorem	s1rn 14562	The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ (𝐴 ∈ 𝑉 → ran ⟨“𝐴”⟩ = {𝐴})
Theorem	s1eq 14563	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Theorem	s1eqd 14564	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Theorem	s1cl 14565	A singleton word is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)
⊢ (𝐴 ∈ 𝐵 → ⟨“𝐴”⟩ ∈ Word 𝐵)
Theorem	s1cld 14566	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ ∈ Word 𝐵)
Theorem	s1prc 14567	Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)
⊢ (¬ 𝐴 ∈ V → ⟨“𝐴”⟩ = ⟨“∅”⟩)
Theorem	s1cli 14568	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ ∈ Word V
Theorem	s1len 14569	Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴”⟩) = 1
Theorem	s1nz 14570	A singleton word is not the empty string. (Contributed by Mario Carneiro, 27-Feb-2016.) (Proof shortened by Kyle Wyonch, 18-Jul-2021.)
⊢ ⟨“𝐴”⟩ ≠ ∅
Theorem	s1dm 14571	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
⊢ dom ⟨“𝐴”⟩ = {0}
Theorem	s1dmALT 14572	Alternate version of s1dm 14571, having a shorter proof, but requiring that 𝐴 is a set. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑆 → dom ⟨“𝐴”⟩ = {0})
Theorem	s1fv 14573	Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)
Theorem	lsws1 14574	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (lastS‘⟨“𝐴”⟩) = 𝐴)
Theorem	eqs1 14575	A word of length 1 is a singleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ (♯‘𝑊) = 1) → 𝑊 = ⟨“(𝑊‘0)”⟩)
Theorem	wrdl1exs1 14576*	A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = ⟨“𝑠”⟩)
Theorem	wrdl1s1 14577	A word of length 1 is a singleton word consisting of the first symbol of the word. (Contributed by AV, 22-Jul-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑊 = ⟨“𝑆”⟩ ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 1 ∧ (𝑊‘0) = 𝑆)))
Theorem	s111 14578	The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (⟨“𝑆”⟩ = ⟨“𝑇”⟩ ↔ 𝑆 = 𝑇))
5.7.5  Concatenations with singleton words
Theorem	ccatws1cl 14579	The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
Theorem	ccatws1clv 14580	The concatenation of a word with a singleton word (which can be over a different alphabet) is a word. (Contributed by AV, 5-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ++ ⟨“𝑋”⟩) ∈ Word V)
Theorem	ccat2s1cl 14581	The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩) ∈ Word 𝑉)
Theorem	ccats1alpha 14582	A concatenation of a word with a singleton word is a word over an alphabet 𝑆 iff the symbols of both words belong to the alphabet 𝑆. (Contributed by AV, 27-Mar-2022.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑈) → ((𝐴 ++ ⟨“𝑋”⟩) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆 ∧ 𝑋 ∈ 𝑆)))
Theorem	ccatws1len 14583	The length of the concatenation of a word with a singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 4-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = ((♯‘𝑊) + 1))
Theorem	ccatws1lenp1b 14584	The length of a word is 𝑁 iff the length of the concatenation of the word with a singleton word is 𝑁 + 1. (Contributed by AV, 4-Mar-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) ↔ (♯‘𝑊) = 𝑁))
Theorem	wrdlenccats1lenm1 14585	The length of a word is the length of the word concatenated with a singleton word minus 1. (Contributed by AV, 28-Jun-2018.) (Revised by AV, 5-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → ((♯‘(𝑊 ++ ⟨“𝑆”⟩)) − 1) = (♯‘𝑊))
Theorem	ccat2s1len 14586	The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 14-Jan-2024.)
⊢ (♯‘(⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)) = 2
Theorem	ccatw2s1cl 14587	The concatenation of a word with two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) ∈ Word 𝑉)
Theorem	ccatw2s1len 14588	The length of the concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 5-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (♯‘((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)) = ((♯‘𝑊) + 2))
Theorem	ccats1val1 14589	Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by JJ, 20-Jan-2024.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑆”⟩)‘𝐼) = (𝑊‘𝐼))
Theorem	ccats1val2 14590	Value of the symbol concatenated with a word. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Proof shortened by Alexander van der Vekens, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ 𝐼 = (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑆”⟩)‘𝐼) = 𝑆)
Theorem	ccat1st1st 14591	The first symbol of a word concatenated with its first symbol is the first symbol of the word. This theorem holds even if 𝑊 is the empty word. (Contributed by AV, 26-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘0) = (𝑊‘0))
Theorem	ccat2s1p1 14592	Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 20-Jan-2024.)
⊢ (𝑋 ∈ 𝑉 → ((⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)‘0) = 𝑋)
Theorem	ccat2s1p2 14593	Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 20-Jan-2024.)
⊢ (𝑌 ∈ 𝑉 → ((⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)‘1) = 𝑌)
Theorem	ccatw2s1ass 14594	Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) = (𝑊 ++ (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)))
Theorem	ccatws1n0 14595	The concatenation of a word with a singleton word is not the empty set. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 5-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ++ ⟨“𝑋”⟩) ≠ ∅)
Theorem	ccatws1ls 14596	The last symbol of the concatenation of a word with a singleton word is the symbol of the singleton word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩)‘(♯‘𝑊)) = 𝑋)
Theorem	lswccats1 14597	The last symbol of a word concatenated with a singleton word is the symbol of the singleton word. (Contributed by AV, 6-Aug-2018.) (Proof shortened by AV, 22-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑆”⟩)) = 𝑆)
Theorem	lswccats1fst 14598	The last symbol of a nonempty word concatenated with its first symbol is the first symbol. (Contributed by AV, 28-Jun-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (lastS‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0))
Theorem	ccatw2s1p1 14599	Extract the symbol of the first singleton word of a word concatenated with this singleton word and another singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof shortened by AV, 1-May-2020.) (Revised by AV, 1-May-2020.) (Revised by AV, 29-Jan-2024.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁 ∧ 𝑋 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑁) = 𝑋)
Theorem	ccatw2s1p2 14600	Extract the second of two single symbols concatenated with a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 + 1)) = 𝑌)