P. 146 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

hashbclem 14501*

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

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

Theorem

hashbc 14502*

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). (Contributed by Mario Carneiro, 13-Jul-2014.)

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

Theorem

hashfacen 14503*

The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by AV, 7-Aug-2024.)

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

Theorem

hashf1lem1 14504*

Lemma for hashf1 14506. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.)

⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵)    ⇒   ⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝐹))

Theorem

hashf1lem2 14505*

Lemma for hashf1 14506. (Contributed by Mario Carneiro, 17-Apr-2015.)

⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))    ⇒   ⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})))

Theorem

hashf1 14506*

The permutation number ∣ 𝐴 ∣ ! · ( ∣ 𝐵 ∣ C ∣ 𝐴 ∣ ) = ∣ 𝐵 ∣ ! / ( ∣ 𝐵 ∣ − ∣ 𝐴 ∣ )! counts the number of injections from 𝐴 to 𝐵. (Contributed by Mario Carneiro, 21-Jan-2015.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))

Theorem

hashfac 14507*

A factorial counts the number of bijections on a finite set. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by Mario Carneiro, 17-Apr-2015.)

⊢ (𝐴 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐴}) = (!‘(♯‘𝐴)))

Theorem

leiso 14508

Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)

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

Theorem

leisorel 14509

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

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

Theorem

fz1isolem 14510*

Lemma for fz1iso 14511. (Contributed by Mario Carneiro, 2-Apr-2014.)

⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)    &   ⊢ 𝐵 = (ℕ ∩ (^◡ < “ {((♯‘𝐴) + 1)}))    &   ⊢ 𝐶 = (ω ∩ (^◡𝐺‘((♯‘𝐴) + 1)))    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))

Theorem

fz1iso 14511*

Any finite ordered set has an order isomorphism to a one-based finite sequence. (Contributed by Mario Carneiro, 2-Apr-2014.)

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

Theorem

ishashinf 14512*

Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 9323. (Contributed by Thierry Arnoux, 5-Jul-2017.)

⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ℕ ∃𝑥 ∈ 𝒫 𝐴(♯‘𝑥) = 𝑛)

Theorem

seqcoll 14513*

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

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

Theorem

seqcoll2 14514*

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, 13-Dec-2014.)

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

Theorem

phphashd 14515

Corollary of the Pigeonhole Principle using equality. Equivalent of phpeqd 9278 expressed using the hash function. (Contributed by Rohan Ridenour, 3-Aug-2023.)

⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)

Theorem

phphashrd 14516

Corollary of the Pigeonhole Principle using equality. Equivalent of phphashd 14515 with reversed arguments. (Contributed by Rohan Ridenour, 3-Aug-2023.)

⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)

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

Theorem

hashprlei 14517

An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.)

⊢ ({𝐴, 𝐵} ∈ Fin ∧ (♯‘{𝐴, 𝐵}) ≤ 2)

Theorem

hash2pr 14518*

A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.)

⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 2) → ∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏})

Theorem

hash2prde 14519*

A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017.)

⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 2) → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))

Theorem

hash2exprb 14520*

A set of size two is an unordered pair if and only if it contains two different elements. (Contributed by Alexander van der Vekens, 14-Jan-2018.)

⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 2 ↔ ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏})))

Theorem

hash2prb 14521*

A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.)

⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 2 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏})))

Theorem

prprrab 14522

The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020.)

⊢ {𝑥 ∈ (𝒫 𝐴 ∖ {∅}) ∣ (♯‘𝑥) = 2} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 2}

Theorem

nehash2 14523

The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.)

⊢ (𝜑 → 𝑃 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 2 ≤ (♯‘𝑃))

Theorem

hash2prd 14524

A set of size two is an unordered pair if it contains two different elements. (Contributed by Alexander van der Vekens, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.)

⊢ ((𝑃 ∈ 𝑉 ∧ (♯‘𝑃) = 2) → ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑃 = {𝑋, 𝑌}))

Theorem

hash2pwpr 14525

If the size of a subset of an unordered pair is 2, the subset is the pair itself. (Contributed by Alexander van der Vekens, 9-Dec-2018.)

⊢ (((♯‘𝑃) = 2 ∧ 𝑃 ∈ 𝒫 {𝑋, 𝑌}) → 𝑃 = {𝑋, 𝑌})

Theorem

hashle2pr 14526*

A nonempty set of size less than or equal to two is an unordered pair of sets. (Contributed by AV, 24-Nov-2021.)

⊢ ((𝑃 ∈ 𝑉 ∧ 𝑃 ≠ ∅) → ((♯‘𝑃) ≤ 2 ↔ ∃𝑎∃𝑏 𝑃 = {𝑎, 𝑏}))

Theorem

hashle2prv 14527*

A nonempty subset of a powerset of a class 𝑉 has size less than or equal to two iff it is an unordered pair of elements of 𝑉. (Contributed by AV, 24-Nov-2021.)

⊢ (𝑃 ∈ (𝒫 𝑉 ∖ {∅}) → ((♯‘𝑃) ≤ 2 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑃 = {𝑎, 𝑏}))

Theorem

pr2pwpr 14528*

The set of subsets of a pair having length 2 is the set of the pair as singleton. (Contributed by AV, 9-Dec-2018.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝑝 ∈ 𝒫 {𝐴, 𝐵} ∣ 𝑝 ≈ 2_o} = {{𝐴, 𝐵}})

Theorem

hashge2el2dif 14529*

A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019.)

⊢ ((𝐷 ∈ 𝑉 ∧ 2 ≤ (♯‘𝐷)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦)

Theorem

hashge2el2difr 14530*

A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020.)

⊢ ((𝐷 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) → 2 ≤ (♯‘𝐷))

Theorem

hashge2el2difb 14531*

A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020.)

⊢ (𝐷 ∈ 𝑉 → (2 ≤ (♯‘𝐷) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦))

Theorem

hashdmpropge2 14532

The size of the domain of a class which contains two ordered pairs with different first components is greater than or equal to 2. (Contributed by AV, 12-Nov-2021.)

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

Theorem

hashtplei 14533

An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015.)

⊢ ({𝐴, 𝐵, 𝐶} ∈ Fin ∧ (♯‘{𝐴, 𝐵, 𝐶}) ≤ 3)

Theorem

hashtpg 14534

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

Theorem

hash7g 14535

The size of an unordered set of seven different elements. (Contributed by AV, 2-Aug-2025.)

⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐷 ∈ 𝑉 ∧ (𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉)) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺)) ∧ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ (𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺)) ∧ (𝐶 ≠ 𝐷 ∧ (𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺))) ∧ ((𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺) ∧ (𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺)))) → (♯‘(({𝐴, 𝐵, 𝐶} ∪ {𝐷}) ∪ {𝐸, 𝐹, 𝐺})) = 7)

Theorem

hashge3el3dif 14536*

A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif 14529, which has an elementary proof, the dominance relation and 1-1 functions from a set with three elements which are known to be different are used to prove this theorem. Although there is also an elementary proof for this theorem, it might be much longer. After all, this proof should be kept because it can be used as template for proofs for higher cardinalities. (Contributed by AV, 20-Mar-2019.) (Proof modification is discouraged.)

⊢ ((𝐷 ∈ 𝑉 ∧ 3 ≤ (♯‘𝐷)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧))

Theorem

elss2prb 14537*

An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020.)

⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (♯‘𝑧) = 2} ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))

Theorem

hash2sspr 14538*

A subset of size two is an unordered pair of elements of its superset. (Contributed by Alexander van der Vekens, 12-Jul-2017.) (Proof shortened by AV, 4-Nov-2020.)

⊢ ((𝑃 ∈ 𝒫 𝑉 ∧ (♯‘𝑃) = 2) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑃 = {𝑎, 𝑏})

Theorem

exprelprel 14539*

If there is an element of the set of subsets with two elements in a set, an unordered pair of sets is in the set. (Contributed by Alexander van der Vekens, 12-Jul-2018.)

⊢ (∃𝑝 ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}𝑝 ∈ 𝑋 → ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ 𝑉 {𝑣, 𝑤} ∈ 𝑋)

Theorem

hash3tr 14540*

A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.)

⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐})

Theorem

hash1to3 14541*

If the size of a set is between 1 and 3 (inclusively), the set is a singleton or an unordered pair or an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.)

⊢ ((𝑉 ∈ Fin ∧ 1 ≤ (♯‘𝑉) ∧ (♯‘𝑉) ≤ 3) → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))

Theorem

hash3tpde 14542*

A set of size three is an unordered triple of three different elements. (Contributed by AV, 21-Jul-2025.)

⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ∧ 𝑉 = {𝑎, 𝑏, 𝑐}))

Theorem

hash3tpexb 14543*

A set of size three is an unordered triple if and only if it contains three different elements. (Contributed by AV, 21-Jul-2025.)

⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 3 ↔ ∃𝑎∃𝑏∃𝑐((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ∧ 𝑉 = {𝑎, 𝑏, 𝑐})))

Theorem

hash3tpb 14544*

A set of size three is a proper unordered triple. (Contributed by AV, 21-Jul-2025.)

⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 3 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ∧ 𝑉 = {𝑎, 𝑏, 𝑐})))

Theorem

tpf1ofv0 14545*

The value of a one-to-one function onto a triple at 0. (Contributed by AV, 20-Jul-2025.)

⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶)))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹‘0) = 𝐴)

Theorem

tpf1ofv1 14546*

The value of a one-to-one function onto a triple at 1. (Contributed by AV, 20-Jul-2025.)

⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶)))    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐹‘1) = 𝐵)

Theorem

tpf1ofv2 14547*

The value of a one-to-one function onto a triple at 2. (Contributed by AV, 20-Jul-2025.)

⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶)))    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝐹‘2) = 𝐶)

Theorem

tpf 14548*

A function into a (proper) triple. (Contributed by AV, 20-Jul-2025.)

⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶)))    &   ⊢ 𝑇 = {𝐴, 𝐵, 𝐶}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐹:(0..^3)⟶𝑇)

Theorem

tpfo 14549*

A function onto a (proper) triple. (Contributed by AV, 20-Jul-2025.)

⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶)))    &   ⊢ 𝑇 = {𝐴, 𝐵, 𝐶}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐹:(0..^3)–onto→𝑇)

Theorem

tpf1o 14550*

A bijection onto a (proper) triple. (Contributed by AV, 21-Jul-2025.)

⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶)))    &   ⊢ 𝑇 = {𝐴, 𝐵, 𝐶}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (♯‘𝑇) = 3) → 𝐹:(0..^3)–1-1-onto→𝑇)

5.6.11.2  Functions with a domain containing at least two different elements

Theorem

fundmge2nop0 14551

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

⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (♯‘dom 𝐺)) → ¬ 𝐺 ∈ (V × V))

Theorem

fundmge2nop 14552

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 ≤ (♯‘dom 𝐺)) → ¬ 𝐺 ∈ (V × V))

Theorem

fun2dmnop0 14553

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

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

Theorem

fun2dmnop 14554

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

5.6.11.3  Finite induction on the size of the first component of a binary relation

Theorem

hashdifsnp1 14555

If the size of a set is a nonnegative integer increased by 1, the size of the set with one of its elements removed is this nonnegative integer. (Contributed by Alexander van der Vekens, 7-Jan-2018.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ∧ 𝑌 ∈ ℕ₀) → ((♯‘𝑉) = (𝑌 + 1) → (♯‘(𝑉 ∖ {𝑁})) = 𝑌))

Theorem

fi1uzind 14556*

Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as ordered pairs of vertices and edges) with a finite number of vertices, usually with 𝐿 = 0 (see opfi1ind 14561) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.)

⊢ 𝐹 ∈ V    &   ⊢ 𝐿 ∈ ℕ₀    &   ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑))    &   ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃))    &   ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌)    &   ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒))    &   ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (♯‘𝑣) = 𝐿) → 𝜓)    &   ⊢ ((((𝑦 + 1) ∈ ℕ₀ ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓)    ⇒   ⊢ (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑)

Theorem

brfi1uzind 14557*

Properties of a binary relation with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with 𝐿 = 0 (see brfi1ind 14558) or 𝐿 = 1. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Proof shortened by AV, 23-Oct-2020.) (Revised by AV, 28-Mar-2021.)

⊢ Rel 𝐺    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝐿 ∈ ℕ₀    &   ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑))    &   ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃))    &   ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹)    &   ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒))    &   ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝐿) → 𝜓)    &   ⊢ ((((𝑦 + 1) ∈ ℕ₀ ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓)    ⇒   ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑)

Theorem

brfi1ind 14558*

Properties of a binary relation with a finite first component, proven by finite induction on the size of the first component. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Revised by AV, 28-Mar-2021.)

⊢ Rel 𝐺    &   ⊢ 𝐹 ∈ V    &   ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑))    &   ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃))    &   ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹)    &   ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒))    &   ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓)    &   ⊢ ((((𝑦 + 1) ∈ ℕ₀ ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓)    ⇒   ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑)

Theorem

brfi1indALT 14559*

Alternate proof of brfi1ind 14558, which does not use brfi1uzind 14557. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ Rel 𝐺    &   ⊢ 𝐹 ∈ V    &   ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑))    &   ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃))    &   ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹)    &   ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒))    &   ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓)    &   ⊢ ((((𝑦 + 1) ∈ ℕ₀ ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓)    ⇒   ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑)

Theorem

opfi1uzind 14560*

Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as ordered pairs of vertices and edges) with a finite number of vertices, usually with 𝐿 = 0 (see opfi1ind 14561) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.)

⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝐿 ∈ ℕ₀    &   ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑))    &   ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃))    &   ⊢ ((⟨𝑣, 𝑒⟩ ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → ⟨(𝑣 ∖ {𝑛}), 𝐹⟩ ∈ 𝐺)    &   ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒))    &   ⊢ ((⟨𝑣, 𝑒⟩ ∈ 𝐺 ∧ (♯‘𝑣) = 𝐿) → 𝜓)    &   ⊢ ((((𝑦 + 1) ∈ ℕ₀ ∧ (⟨𝑣, 𝑒⟩ ∈ 𝐺 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓)    ⇒   ⊢ ((⟨𝑉, 𝐸⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑)

Theorem

opfi1ind 14561*

Properties of an ordered pair with a finite first component, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as ordered pairs of vertices and edges) with a finite number of vertices, e.g., fusgrfis 29365. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.)

⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    &   ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑))    &   ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃))    &   ⊢ ((⟨𝑣, 𝑒⟩ ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → ⟨(𝑣 ∖ {𝑛}), 𝐹⟩ ∈ 𝐺)    &   ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒))    &   ⊢ ((⟨𝑣, 𝑒⟩ ∈ 𝐺 ∧ (♯‘𝑣) = 0) → 𝜓)    &   ⊢ ((((𝑦 + 1) ∈ ℕ₀ ∧ (⟨𝑣, 𝑒⟩ ∈ 𝐺 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓)    ⇒   ⊢ ((⟨𝑉, 𝐸⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin) → 𝜑)

5.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 14563, see, for example, s1cli 14653: ⟨“𝐴”⟩ ∈ Word V. Note that the empty word ∅ (i.e., the empty set) is the only word over an empty alphabet, see 0wrd0 14588. 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-hash 14380: (♯‘𝑊)	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 6581: (𝑊‘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 14611: (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 14689: (𝑊 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 14619: (𝑊 ++ 𝑈)	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.
Reversal of a word	df-reverse 14807: (reverse‘𝑊)	Operation which reverses the order of symbols in a word.	(𝑊 ∈ Word 𝑉 → (♯‘(reverse‘𝑊)) = (♯‘𝑊))
Cyclical shift of a word	df-csh 14837: (𝑊 cyclShift 𝑁)	Operation cyclically shifting the symbols by a number of positions.	(𝑊 ∈ Word 𝑉 → (𝑊 cyclShift (♯‘𝑊)) = 𝑊)
Splicing of a word	df-splice 14798: (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)	Operation which replaces portions of words.	((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) ∈ Word 𝐴)
Singleton word	df-s1 14644: ⟨“𝑆”⟩	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 𝐿.

5.7.1  Definitions and basic theorems

Syntax

cword 14562

Syntax for the Word operator.

class Word 𝑆

Definition

df-word 14563*

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 (see frmdval 18886). (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 14564*

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

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 𝑆 = ∪ 𝑙 ∈ ℕ₀ (𝑆 ↑_m (0..^𝑙)))

Theorem

iswrdi 14566

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

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

Theorem

wrdf 14567

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

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

Theorem

iswrdb 14568

A word over an alphabet is a function from an open range of nonnegative integers (of length equal to the length of the word) into the alphabet. (Contributed by Alexander van der Vekens, 30-Jul-2018.)

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

Theorem

wrddm 14569

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 14570

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 14571

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 14572

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 14573

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 14574

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

⊢ 𝑆 ∈ V    ⇒   ⊢ Word 𝑆 ∈ V

Theorem

wrdsymbcl 14575

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 14576

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 14577

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 14578

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

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 14580

A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015.) (Proof shortened by AV, 18-Nov-2018.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin)

Theorem

lencl 14581

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

lennncl 14582

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

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

Theorem

wrdffz 14583

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

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

Theorem

wrdeq 14584

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

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

Theorem

wrdeqi 14585

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

⊢ 𝑆 = 𝑇    ⇒   ⊢ Word 𝑆 = Word 𝑇

Theorem

iswrddm0 14586

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

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

Theorem

wrd0 14587

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 14588

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

⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅)

Theorem

ffz0iswrd 14589

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 14590

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

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

Theorem

nfwrd 14591

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

⊢ Ⅎ𝑥𝑆    ⇒   ⊢ Ⅎ𝑥Word 𝑆

Theorem

csbwrdg 14592*

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

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

Theorem

wrdnval 14593*

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 𝑉 ∣ (♯‘𝑤) = 𝑁} = (𝑉 ↑_m (0..^𝑁)))

Theorem

wrdmap 14594

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

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

Theorem

hashwrdn 14595*

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 ∧ 𝑁 ∈ ℕ₀) → (♯‘{𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁}) = ((♯‘𝑉)↑𝑁))

Theorem

wrdnfi 14596*

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 14597

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 14598

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

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

Theorem

len0nnbi 14599

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

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

Theorem

wrdlenge2n0 14600

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 ≤ (♯‘𝑊)) → 𝑊 ≠ ∅)