| Metamath
Proof Explorer Theorem List (p. 146 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fz1iso 14501* | 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 14502* | Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 9296. (Contributed by Thierry Arnoux, 5-Jul-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ℕ ∃𝑥 ∈ 𝒫 𝐴(♯‘𝑥) = 𝑛) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | seqcoll 14503* | 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 14504* | 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 14505 | Corollary of the Pigeonhole Principle using equality. Equivalent of phpeqd 9252 expressed using the hash function. (Contributed by Rohan Ridenour, 3-Aug-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | phphashrd 14506 | Corollary of the Pigeonhole Principle using equality. Equivalent of phphashd 14505 with reversed arguments. (Contributed by Rohan Ridenour, 3-Aug-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashprlei 14507 | An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ({𝐴, 𝐵} ∈ Fin ∧ (♯‘{𝐴, 𝐵}) ≤ 2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hash2pr 14508* | A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 2) → ∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hash2prde 14509* | 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 14510* | 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 14511* | A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 2 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | prprrab 14512 | 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 14513 | The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝜑 → 𝑃 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hash2prd 14514 | 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 14515 | 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 14516* | 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 14517* | 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 14518* | The set of subsets of a pair having length 2 is the set of the pair as singleton. (Contributed by AV, 9-Dec-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝑝 ∈ 𝒫 {𝐴, 𝐵} ∣ 𝑝 ≈ 2o} = {{𝐴, 𝐵}}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashge2el2dif 14519* | A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝐷 ∈ 𝑉 ∧ 2 ≤ (♯‘𝐷)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashge2el2difr 14520* | A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝐷 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) → 2 ≤ (♯‘𝐷)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashge2el2difb 14521* | A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝐷 ∈ 𝑉 → (2 ≤ (♯‘𝐷) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashdmpropge2 14522 | 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 14523 | An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ({𝐴, 𝐵, 𝐶} ∈ Fin ∧ (♯‘{𝐴, 𝐵, 𝐶}) ≤ 3) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashtpg 14524 | 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 14525 | The size of an unordered set of seven different elements. (Contributed by AV, 2-Aug-2025.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐷 ∈ 𝑉 ∧ (𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉)) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺)) ∧ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ (𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺)) ∧ (𝐶 ≠ 𝐷 ∧ (𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺))) ∧ ((𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺) ∧ (𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺)))) → (♯‘(({𝐴, 𝐵, 𝐶} ∪ {𝐷}) ∪ {𝐸, 𝐹, 𝐺})) = 7) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashge3el3dif 14526* | A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif 14519, 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 14527* | An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (♯‘𝑧) = 2} ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hash2sspr 14528* | 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 14529* | 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 14530* | A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hash1to3 14531* | 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 14532* | A set of size three is an unordered triple of three different elements. (Contributed by AV, 21-Jul-2025.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ∧ 𝑉 = {𝑎, 𝑏, 𝑐})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hash3tpexb 14533* | 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 14534* | A set of size three is a proper unordered triple. (Contributed by AV, 21-Jul-2025.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 3 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ∧ 𝑉 = {𝑎, 𝑏, 𝑐}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | tpf1ofv0 14535* | 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 14536* | 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 14537* | 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 14538* | A function into a (proper) triple. (Contributed by AV, 20-Jul-2025.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶))) & ⊢ 𝑇 = {𝐴, 𝐵, 𝐶} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐹:(0..^3)⟶𝑇) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | tpfo 14539* | A function onto a (proper) triple. (Contributed by AV, 20-Jul-2025.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶))) & ⊢ 𝑇 = {𝐴, 𝐵, 𝐶} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐹:(0..^3)–onto→𝑇) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | tpf1o 14540* | A bijection onto a (proper) triple. (Contributed by AV, 21-Jul-2025.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶))) & ⊢ 𝑇 = {𝐴, 𝐵, 𝐶} ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (♯‘𝑇) = 3) → 𝐹:(0..^3)–1-1-onto→𝑇) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fundmge2nop0 14541 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop 14542 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see structn0fun 17188. (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 14542 | 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 14543 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop 14544 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see structn0fun 17188. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → ¬ 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fun2dmnop 14544 | 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)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashdifsnp1 14545 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) → ((♯‘𝑉) = (𝑌 + 1) → (♯‘(𝑉 ∖ {𝑁})) = 𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fi1uzind 14546* | 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 14551) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (♯‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | brfi1uzind 14547* | 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 14548) 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 & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | brfi1ind 14548* | 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) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | brfi1indALT 14549* | Alternate proof of brfi1ind 14548, which does not use brfi1uzind 14547. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ Rel 𝐺 & ⊢ 𝐹 ∈ V & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | opfi1uzind 14550* | 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 14551) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((〈𝑉, 𝐸〉 ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | opfi1ind 14551* | 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 29347. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((〈𝑉, 𝐸〉 ∈ 𝐺 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
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 14553, see, for example, s1cli 14643: 〈“𝐴”〉 ∈ Word V. Note that the empty word ∅ (i.e., the empty set) is the only word over an empty alphabet, see 0wrd0 14578. 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:
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Syntax | cword 14552 | Syntax for the Word operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
| class Word 𝑆 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Definition | df-word 14553* | 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 ℕ0 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 18864). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | iswrd 14554* | 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 𝑊:(0..^𝑙)⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrdval 14555* | 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 (𝑆 ↑m (0..^𝑙))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | iswrdi 14556 | 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 14557 | A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | iswrdb 14558 | 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 14559 | 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 14560 | 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 14561 | 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 14562 | 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 14563 | 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 14564 | The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝑆 ∈ V ⇒ ⊢ Word 𝑆 ∈ V | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrdsymbcl 14565 | 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 14566 | 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 14567 | 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 14568 | 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 14569* | 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 14570 | 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 14571 | 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 𝑆 → (♯‘𝑊) ∈ ℕ0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | lennncl 14572 | The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrdffz 14573 | A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrdeq 14574 | Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrdeqi 14575 | Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝑆 = 𝑇 ⇒ ⊢ Word 𝑆 = Word 𝑇 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | iswrddm0 14576 | A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrd0 14577 | 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 14578 | The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | ffz0iswrd 14579 | 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 14580 | A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nfwrd 14581 | Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ Ⅎ𝑥𝑆 ⇒ ⊢ Ⅎ𝑥Word 𝑆 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | csbwrdg 14582* | Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrdnval 14583* | 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 14584 | Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑m (0..^𝑁)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | hashwrdn 14585* | 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 14586* | 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 14587 | 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 14588 | A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | len0nnbi 14589 | The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrdlenge2n0 14590 | 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 14591 | 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 14592* | 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 14593 | 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 14594 | 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 14595* | 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 14596* | 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 14597* | 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 14598 | A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wrdred1hash 14599 | 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)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| Syntax | clsw 14600 | Extend class notation with the Last Symbol of a word. | ||||||||||||||||||||||||||||||||||||||||||||||||||
| class lastS | ||||||||||||||||||||||||||||||||||||||||||||||||||||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |