P. 113 of Theorem List - Intuitionistic Logic Explorer

Type

Label

Description

Statement

Theorem

hashprg 11201

The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Revised by AV, 18-Sep-2021.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2))

Theorem

prhash2ex 11202

There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 11208, numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020.)

⊢ (♯‘{0, 1}) = 2

Theorem

hashp1i 11203

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 = suc 𝐴    &   ⊢ (♯‘𝐴) = 𝑀    &   ⊢ (𝑀 + 1) = 𝑁    ⇒   ⊢ (♯‘𝐵) = 𝑁

Theorem

hash1 11204

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ (♯‘1_o) = 1

Theorem

hash2 11205

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ (♯‘2_o) = 2

Theorem

hash3 11206

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ (♯‘3_o) = 3

Theorem

hash4 11207

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ (♯‘4_o) = 4

Theorem

pr0hash2ex 11208

There is (at least) one set with two different elements: the unordered pair containing the empty set and the singleton containing the empty set. (Contributed by AV, 29-Jan-2020.)

⊢ (♯‘{∅, {∅}}) = 2

Theorem

fihashss 11209

The size of a subset is less than or equal to the size of its superset. (Contributed by Alexander van der Vekens, 14-Jul-2018.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘𝐵) ≤ (♯‘𝐴))

Theorem

fiprsshashgt1 11210

The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.)

⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ Fin) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (♯‘𝐶)))

Theorem

fihashssdif 11211

The size of the difference of a finite set and a finite subset is the set's size minus the subset's. (Contributed by Jim Kingdon, 31-May-2022.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘(𝐴 ∖ 𝐵)) = ((♯‘𝐴) − (♯‘𝐵)))

Theorem

hashdifsn 11212

The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (♯‘(𝐴 ∖ {𝐵})) = ((♯‘𝐴) − 1))

Theorem

hashdifpr 11213

The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.)

⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (♯‘(𝐴 ∖ {𝐵, 𝐶})) = ((♯‘𝐴) − 2))

Theorem

hashfz 11214

Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario Carneiro, 15-Apr-2015.)

⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (♯‘(𝐴...𝐵)) = ((𝐵 − 𝐴) + 1))

Theorem

hashfzo 11215

Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (♯‘(𝐴..^𝐵)) = (𝐵 − 𝐴))

Theorem

hashfzo0 11216

Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ (𝐵 ∈ ℕ₀ → (♯‘(0..^𝐵)) = 𝐵)

Theorem

hashfzp1 11217

Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.)

⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (♯‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴))

Theorem

hashfz0 11218

Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)

⊢ (𝐵 ∈ ℕ₀ → (♯‘(0...𝐵)) = (𝐵 + 1))

Theorem

hashxp 11219

The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))

Theorem

hashmap 11220

The size of the set exponential of two finite sets is the exponential of their sizes. (This is the original motivation behind the notation for set exponentiation.) (Contributed by Mario Carneiro, 5-Aug-2014.) (Proof shortened by AV, 18-Jul-2022.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ↑_𝑚 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))

Theorem

hashpwfi 11221

The number of finite subsets of a finite set is two raised to the power of the size of the set. For a similar theorem with set size expressed using equinumerosity, see 2omapfi 7284. For the number of subsets (which need not be finite) of a set, see pw1mapen 16909. (Contributed by Jim Kingdon, 5-Jun-2026.)

⊢ (𝐴 ∈ Fin → (♯‘(𝒫 𝐴 ∩ Fin)) = (2↑(♯‘𝐴)))

Theorem

fimaxq 11222*

A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.)

⊢ ((𝐴 ⊆ ℚ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Theorem

fiubm 11223*

Lemma for fiubz 11224 and fiubnn 11225. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)

⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ ℚ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Theorem

fiubz 11224*

A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)

⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Theorem

fiubnn 11225*

A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)

⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Theorem

resunimafz0 11226

The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)

⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    ⇒   ⊢ (𝜑 → (𝐼 ↾ (𝐹 “ (0...𝑁))) = ((𝐼 ↾ (𝐹 “ (0..^𝑁))) ∪ {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩}))

Theorem

fnfz0hash 11227

The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹 Fn (0...𝑁)) → (♯‘𝐹) = (𝑁 + 1))

Theorem

ffz0hash 11228

The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV, 11-Apr-2021.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹:(0...𝑁)⟶𝐵) → (♯‘𝐹) = (𝑁 + 1))

Theorem

ffzo0hash 11229

The size of a function on a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 25-Mar-2018.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹 Fn (0..^𝑁)) → (♯‘𝐹) = 𝑁)

Theorem

fnfzo0hash 11230

The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹:(0..^𝑁)⟶𝐵) → (♯‘𝐹) = 𝑁)

Theorem

sseqn 11231*

Two ways to express the subsets of a class of a given size. It might seem that {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑁} would suffice, but that would require the converse of hashcl 11172 or something similar. Although each side of the equality would be well defined if we changed 𝑁 ∈ ℕ₀ to 𝑁 ∈ ℤ, they would give different results for the (degenerate) case of a negative size, as shown at ssenneg 11232 and sshashneg 11233. (Contributed by Jim Kingdon, 22-May-2026.)

⊢ (𝑁 ∈ ℕ₀ → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≈ (1...𝑁)} = {𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑁})

Theorem

ssenneg 11232*

Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11233 this shows that sseqn 11231 could not be extended beyond 𝑁 ∈ ℕ₀. (Contributed by Jim Kingdon, 22-May-2026.)

⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 0) → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≈ (1...𝑁)} = {∅})

Theorem

sshashneg 11233*

Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11232 this shows that sseqn 11231 could not be extended beyond 𝑁 ∈ ℕ₀. (Contributed by Jim Kingdon, 22-May-2026.)

⊢ ((𝑁 ∈ ℤ ∧ 𝑁 < 0) → {𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑁} = ∅)

Theorem

hashfibclem 11234*

Lemma for hashfibc 11235: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.)

⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑗}))    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ (𝒫 (𝐴 ∪ {𝑧}) ∩ Fin) ∣ (♯‘𝑥) = 𝐾}))

Theorem

hashfibc 11235*

The binomial coefficient counts the number of subsets of a finite set of a given size. This is Metamath 100 proof #58 (formula for the number of combinations). For more on the notation for subsets of a given size, see sseqn 11231. (Contributed by Mario Carneiro, 13-Jul-2014.)

⊢ ((𝐴 ∈ Fin ∧ 𝐾 ∈ ℤ) → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝐾}))

Theorem

hashfacen 11236*

The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.)

⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})

Theorem

leisorel 11237

Version of isorel 5987 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)

⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^*) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷)))

Theorem

zfz1isolemsplit 11238

Lemma for zfz1iso 11241. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.)

⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}))

Theorem

zfz1isolemiso 11239*

Lemma for zfz1iso 11241. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.)

⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ⊆ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))    &   ⊢ (𝜑 → 𝐴 ∈ (1...(♯‘𝑋)))    &   ⊢ (𝜑 → 𝐵 ∈ (1...(♯‘𝑋)))    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ((𝐺 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝐴) < ((𝐺 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝐵)))

Theorem

zfz1isolem1 11240*

Lemma for zfz1iso 11241. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.)

⊢ (𝜑 → 𝐾 ∈ ω)    &   ⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)))    &   ⊢ (𝜑 → 𝑋 ⊆ ℤ)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≈ suc 𝐾)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))

Theorem

zfz1iso 11241*

A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)

⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝐴)), 𝐴))

Theorem

seq3coll 11242*

The function 𝐹 contains a sparse set of nonzero values to be summed. The function 𝐺 is an order isomorphism from the set of nonzero values of 𝐹 to a 1-based finite sequence, and 𝐻 collects these nonzero values together. Under these conditions, the sum over the values in 𝐻 yields the same result as the sum over the original set 𝐹. (Contributed by Mario Carneiro, 2-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)

⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (𝐻‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))

4.6.10.1  Proper unordered pairs and triples (sets of size 2 and 3)

Theorem

hash2en 11243

Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.)

⊢ (𝑉 ≈ 2_o ↔ (𝑉 ∈ Fin ∧ (♯‘𝑉) = 2))

Theorem

hashdmprop2dom 11244

A class which contains two ordered pairs with different first components has at least two elements. (Contributed by AV, 12-Nov-2021.)

⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ⊆ 𝐹)    ⇒   ⊢ (𝜑 → 2_o ≼ dom 𝐹)

Theorem

hashtpgim 11245

The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.) (Revised by Jim Kingdon, 17-Apr-2026.)

⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (♯‘{𝐴, 𝐵, 𝐶}) = 3))

Theorem

hashtpglem 11246

Lemma for hashtpg 11247. This is one of the three not-equal conclusions required for the reverse direction. (Contributed by Jim Kingdon, 18-Apr-2026.)

⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → (♯‘{𝐴, 𝐵, 𝐶}) = 3)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)

Theorem

hashtpg 11247

The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.)

⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) ↔ (♯‘{𝐴, 𝐵, 𝐶}) = 3))

4.6.10.2  Functions with a domain containing at least two different elements

Theorem

fundm2domnop0 11248

A function with a domain containing (at least) two different elements is not an ordered pair. This theorem (which requires that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see structn0fun 13312. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Proof shortened by AV, 15-Nov-2021.)

⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2_o ≼ dom 𝐺) → ¬ 𝐺 ∈ (V × V))

Theorem

fundm2domnop 11249

A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 12-Oct-2020.) (Proof shortened by AV, 9-Jun-2021.)

⊢ ((Fun 𝐺 ∧ 2_o ≼ dom 𝐺) → ¬ 𝐺 ∈ (V × V))

Theorem

fun2dmnop0 11250

A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop 11251 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see structn0fun 13312. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.)

⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → ¬ 𝐺 ∈ (V × V))

Theorem

fun2dmnop 11251

A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 9-Jun-2021.)

⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((Fun 𝐺 ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → ¬ 𝐺 ∈ (V × V))

4.7  Words over a set

This section is about words (or strings) over a set (alphabet) defined as finite sequences of symbols (or characters) being elements of the alphabet. Although it is often required that the underlying set/alphabet be nonempty, finite and not a proper class, these restrictions are not made in the current definition df-word 11253. Note that the empty word ∅ (i.e., the empty set) is the only word over an empty alphabet, see 0wrd0 11278. The set Word 𝑆 of words over 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word. Besides the definition of words themselves, several operations on words are defined in this section:

Name	Reference	Explanation	Example	Remarks
Length (or size) of a word	df-ihash 11167: (♯‘𝑊)	Operation which determines the number of the symbols within the word.	𝑊:(0..^𝑁)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 𝑁	This is not a special definition for words, but for arbitrary sets.
First symbol of a word	df-fv 5365: (𝑊‘0)	Operation which extracts the first symbol of a word. The result is the symbol at the first place in the sequence representing the word.	𝑊:(0..^1)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (𝑊‘0) ∈ 𝑆	This is not a special definition for words, but for arbitrary functions with a half-open range of nonnegative integers as domain.
Last symbol of a word	df-lsw 11298: (lastS‘𝑊)	Operation which extracts the last symbol of a word. The result is the symbol at the last place in the sequence representing the word.	𝑊:(0..^3)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (lastS‘𝑊) = (𝑊‘2)	Note that the index of the last symbol is less by 1 than the length of the word.
Subword (or substring) of a word	df-substr 11366: (𝑊 substr ⟨𝐼, 𝐽⟩)	Operation which extracts a portion of a word. The result is a consecutive, reindexed part of the sequence representing the word.	𝑊:(0..^3)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (𝑊 substr ⟨1, 2⟩) ∈ Word 𝑆 ∧ (♯‘(𝑊 substr ⟨1, 2⟩)) = 1	Note that the last index of the range defining the subword is greater by 1 than the index of the last symbol of the subword in the sequence of the original word.
Concatenation of two words	df-concat 11307: (𝑊 ++ 𝑈)	Operation combining two words to one new word. The result is a combined, reindexed sequence build from the sequences representing the two words.	(𝑊 ∈ Word 𝑆 ∧ 𝑈 ∈ Word 𝑆) → (♯‘(𝑊 ++ 𝑈)) = ((♯‘𝑊) + (♯‘𝑈))	Note that the index of the first symbol of the second concatenated word is the length of the first word in the concatenation.
Singleton word	df-s1 11332: ⟨“𝑆”⟩	Constructor building a word of length 1 from a symbol.	(♯‘⟨“𝑆”⟩) = 1

Conventions:

• Words are usually represented by class variable 𝑊, or if two words are involved, by 𝑊 and 𝑈 or by 𝐴 and 𝐵.
• The alphabets are usually represented by class variable 𝑉 (because any arbitrary set can be an alphabet), sometimes also by 𝑆 (especially as codomain of the function representing a word, because the alphabet is the set of symbols).
• The symbols are usually represented by class variables 𝑆 or 𝐴, or if two symbols are involved, by 𝑆 and 𝑇 or by 𝐴 and 𝐵.
• The indices of the sequence representing a word are usually represented by class variable 𝐼, if two indices are involved (especially for subwords) by 𝐼 and 𝐽, or by 𝑀 and 𝑁.
• The length of a word is usually represented by class variables 𝑁 or 𝐿.
• The number of positions by which to cyclically shift a word is usually represented by class variables 𝑁 or 𝐿.

4.7.1  Definitions and basic theorems

Syntax

cword 11252

Syntax for the Word operator.

class Word 𝑆

Definition

df-word 11253*

Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) 𝑆. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of ℕ₀ so that two words with the same symbols in the same order be equal. The set Word 𝑆 is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word 𝑆 equipped with concatenation is the free monoid over 𝑆, and the monoid unit is the empty word. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ₀ 𝑤:(0..^𝑙)⟶𝑆}

Theorem

iswrd 11254*

Property of being a word over a set with an existential quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)

⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆)

Theorem

wrdval 11255*

Value of the set of words over a set. (Contributed by Stefan O'Rear, 10-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ (𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ₀ (𝑆 ↑_𝑚 (0..^𝑙)))

Theorem

lencl 11256

The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015.)

⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ₀)

Theorem

iswrdinn0 11257

A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.)

⊢ ((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℕ₀) → 𝑊 ∈ Word 𝑆)

Theorem

wrdf 11258

A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Theorem

iswrdiz 11259

A zero-based sequence is a word. In iswrdinn0 11257 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.)

⊢ ((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℤ) → 𝑊 ∈ Word 𝑆)

Theorem

wrddm 11260

The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020.)

⊢ (𝑊 ∈ Word 𝑆 → dom 𝑊 = (0..^(♯‘𝑊)))

Theorem

sswrd 11261

The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)

⊢ (𝑆 ⊆ 𝑇 → Word 𝑆 ⊆ Word 𝑇)

Theorem

snopiswrd 11262

A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018.) (Proof shortened by AV, 18-Apr-2021.)

⊢ (𝑆 ∈ 𝑉 → {⟨0, 𝑆⟩} ∈ Word 𝑉)

Theorem

wrdexg 11263

The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by JJ, 18-Nov-2022.)

⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V)

Theorem

wrdexb 11264

The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)

⊢ (𝑆 ∈ V ↔ Word 𝑆 ∈ V)

Theorem

wrdexi 11265

The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.)

⊢ 𝑆 ∈ V    ⇒   ⊢ Word 𝑆 ∈ V

Theorem

wrdsymbcl 11266

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 11267

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 11268

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 11269

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 11270*

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 11271

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 11272

The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.)

⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)

Theorem

wrdffz 11273

A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆)

Theorem

wrdeq 11274

Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇)

Theorem

wrdeqi 11275

Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.)

⊢ 𝑆 = 𝑇    ⇒   ⊢ Word 𝑆 = Word 𝑇

Theorem

iswrddm0 11276

A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.)

⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆)

Theorem

wrd0 11277

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 11278

The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)

⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅)

Theorem

ffz0iswrdnn0 11279

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 11280

A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.)

⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆))))

Theorem

nfwrd 11281

Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ Ⅎ𝑥𝑆    ⇒   ⊢ Ⅎ𝑥Word 𝑆

Theorem

csbwrdg 11282*

Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)

⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆)

Theorem

wrdnval 11283*

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.)

⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ₀) → {𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁} = (𝑉 ↑_𝑚 (0..^𝑁)))

Theorem

wrdmap 11284

Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)

⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ₀) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑_𝑚 (0..^𝑁))))

Theorem

wrdsymb0 11285

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 11286

A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)

⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊)))

Theorem

len0nnbi 11287

The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.)

⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ))

Theorem

wrdlenge2n0 11288

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 11289

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 11290*

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 11291

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 11292

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 11293*

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 11294*

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 11295

A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)

⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆)

Theorem

wrdred1hash 11296

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 11297

Extend class notation with the Last Symbol of a word.

class lastS

Definition

df-lsw 11298

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 11299

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 11300

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‘𝑊) = ∅)