P. 114 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11301-11400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wrdsymbcl 11301	A symbol within a word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝐼) ∈ 𝑉)
Theorem	wrdfn 11302	A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018.)
⊢ (𝑊 ∈ Word 𝑆 → 𝑊 Fn (0..^(♯‘𝑊)))
Theorem	wrdv 11303	A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) (Proof shortened by JJ, 18-Nov-2022.)
⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V)
Theorem	wrdlndm 11304	The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021.) (Proof shortened by JJ, 18-Nov-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∉ dom 𝑊)
Theorem	iswrdsymb 11305*	An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021.)
⊢ ((𝑊 ∈ Word V ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ∈ 𝑉) → 𝑊 ∈ Word 𝑉)
Theorem	wrdfin 11306	A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015.) (Proof shortened by AV, 18-Nov-2018.)
⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin)
Theorem	lennncl 11307	The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)
Theorem	wrdffz 11308	A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.)
⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆)
Theorem	wrdeq 11309	Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇)
Theorem	wrdeqi 11310	Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.)
⊢ 𝑆 = 𝑇    ⇒   ⊢ Word 𝑆 = Word 𝑇
Theorem	iswrddm0 11311	A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.)
⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆)
Theorem	wrd0 11312	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 11313	The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)
⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅)
Theorem	ffz0iswrdnn0 11314	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...𝐿)⟶𝑆 ∧ 𝐿 ∈ ℕ0) → 𝑊 ∈ Word 𝑆)
Theorem	wrdsymb 11315	A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.)
⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆))))
Theorem	nfwrd 11316	Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ Ⅎ𝑥𝑆    ⇒   ⊢ Ⅎ𝑥Word 𝑆
Theorem	csbwrdg 11317*	Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆)
Theorem	wrdnval 11318*	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 𝑉 ∣ (♯‘𝑤) = 𝑁} = (𝑉 ↑𝑚 (0..^𝑁)))
Theorem	wrdmap 11319	Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑𝑚 (0..^𝑁))))
Theorem	wrdsymb0 11320	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 11321	A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊)))
Theorem	len0nnbi 11322	The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ))
Theorem	wrdlenge2n0 11323	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 11324	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 11325*	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 11326	The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉)
Theorem	fstwrdne0 11327	The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)) → (𝑊‘0) ∈ 𝑉)
Theorem	eqwrd 11328*	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 11329*	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	wrdred1 11330	A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)
⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆)
Theorem	wrdred1hash 11331	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))
4.7.2  Last symbol of a word
Syntax	clsw 11332	Extend class notation with the Last Symbol of a word.
class lastS
Definition	df-lsw 11333	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	lswwrd 11334	Extract the last symbol of a word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Jim Kingdon, 18-Dec-2025.)
⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
Theorem	lsw0 11335	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 11336	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)
⊢ (lastS‘∅) = ∅
Theorem	lsw1 11337	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 11338	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	lswex 11339	Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11336 or lswcl 11338 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.)
⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) ∈ V)
Theorem	lswlgt0cl 11340	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‘𝑊) ∈ 𝑉)
4.7.3  Concatenations of words
Syntax	cconcat 11341	Syntax for the concatenation operator.
class ++
Definition	df-concat 11342*	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	ccatfvalfi 11343*	Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ Fin ∧ 𝑇 ∈ Fin) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))))
Theorem	ccatcl 11344	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	ccatclab 11345	The concatenation of words over two sets is a word over the union of those sets. (Contributed by Jim Kingdon, 19-Dec-2025.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word (𝐴 ∪ 𝐵))
Theorem	ccatlen 11346	The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇)))
Theorem	ccat0 11347	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 11348	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 11349	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 11350	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 11351	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 11352	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	ccatsymb 11353	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 11354	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 11355	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 11356	The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0))
Theorem	ccatlid 11357	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 11358	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 11359	Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈)))
Theorem	ccatrn 11360	The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇))
Theorem	ccatidid 11361	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
⊢ (∅ ++ ∅) = ∅
Theorem	lswccatn0lsw 11362	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 11363	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 11364	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 11365	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 𝑆)
4.7.4  Singleton words
Syntax	cs1 11366	Syntax for the singleton word constructor.
class ⟨“𝐴”⟩
Definition	df-s1 11367	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 11374, and not, as maybe expected, the empty word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Theorem	s1val 11368	Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝑉 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
Theorem	s1rn 11369	The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ (𝐴 ∈ 𝑉 → ran ⟨“𝐴”⟩ = {𝐴})
Theorem	s1eq 11370	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Theorem	s1eqd 11371	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Theorem	s1cl 11372	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 11373	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ ∈ Word 𝐵)
Theorem	s1prc 11374	Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)
⊢ (¬ 𝐴 ∈ V → ⟨“𝐴”⟩ = ⟨“∅”⟩)
Theorem	s1leng 11375	Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝑉 → (♯‘⟨“𝐴”⟩) = 1)
Theorem	s1dmg 11376	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
⊢ (𝐴 ∈ 𝑆 → dom ⟨“𝐴”⟩ = {0})
Theorem	s1fv 11377	Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)
Theorem	lsws1 11378	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (lastS‘⟨“𝐴”⟩) = 𝐴)
Theorem	eqs1 11379	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 11380*	A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = ⟨“𝑠”⟩)
Theorem	wrdl1s1 11381	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 11382	The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (⟨“𝑆”⟩ = ⟨“𝑇”⟩ ↔ 𝑆 = 𝑇))
4.7.5  Concatenations with singleton words
Theorem	ccatws1cl 11383	The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
Theorem	ccat2s1cl 11384	The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩) ∈ Word 𝑉)
Theorem	ccatws1leng 11385	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	ccatws1lenp1bg 11386	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	wrdlenccats1lenm1g 11387	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	ccatw2s1cl 11388	The concatenation of a word with two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) ∈ Word 𝑉)
Theorem	ccatw2s1leng 11389	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	ccats1val1g 11390	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 11391	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 11392	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	ccatws1ls 11393	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 11394	The last symbol of a word concatenated with a singleton word is the symbol of the singleton word. (Contributed by AV, 6-Aug-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑆”⟩)) = 𝑆)
Theorem	lswccats1fst 11395	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	ccatw2s1p1g 11396	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 11397	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)) = 𝑌)
Theorem	ccat2s1fvwd 11398	Extract a symbol of a word from the concatenation of the word with two single symbols. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 13-Jan-2020.) (Proof shortened by AV, 1-May-2020.) (Revised by AV, 28-Jan-2024.)
⊢ (𝜑 → 𝑊 ∈ Word 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐼 < (♯‘𝑊))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝐼) = (𝑊‘𝐼))
Theorem	ccat2s1fstg 11399	The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 28-Jan-2024.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘0) = (𝑊‘0))
4.7.6  Subwords/substrings
Syntax	csubstr 11400	Syntax for the subword operator.
class substr