Home | Metamath
Proof Explorer Theorem List (p. 132 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | leisorel 13101 | Version of isorel 6476 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1isolem 13102* | Lemma for fz1iso 13103. (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) & ⊢ 𝐵 = (ℕ ∩ (◡ < “ {((#‘𝐴) + 1)})) & ⊢ 𝐶 = (ω ∩ (◡𝐺‘((#‘𝐴) + 1))) & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1iso 13103* | Any finite ordered set has an order isometry to a one-based finite sequence. (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ishashinf 13104* | Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 8058. (Contributed by Thierry Arnoux, 5-Jul-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ℕ ∃𝑥 ∈ 𝒫 𝐴(#‘𝑥) = 𝑛) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | seqcoll 13105* | 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 13106* | 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 | hashprlei 13107 | An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({𝐴, 𝐵} ∈ Fin ∧ (#‘{𝐴, 𝐵}) ≤ 2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2pr 13108* | A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ (#‘𝑉) = 2) → ∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prde 13109* | 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 13110* | 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 13111* | A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 ∈ 𝑊 → ((#‘𝑉) = 2 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | prprrab 13112 | 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 13113 | The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝑃 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 2 ≤ (#‘𝑃)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prd 13114 | 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, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑃 ∈ 𝑉 ∧ (#‘𝑃) = 2) → ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑃 = {𝑋, 𝑌})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2pwpr 13115 | 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 | pr2pwpr 13116* | 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𝑜} = {{𝐴, 𝐵}}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2dif 13117* | A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐷 ∈ 𝑉 ∧ 2 ≤ (#‘𝐷)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difr 13118* | A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐷 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) → 2 ≤ (#‘𝐷)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difb 13119* | A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐷 ∈ 𝑉 → (2 ≤ (#‘𝐷) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashtplei 13120 | An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({𝐴, 𝐵, 𝐶} ∈ Fin ∧ (#‘{𝐴, 𝐵, 𝐶}) ≤ 3) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashtpg 13121 | 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 | hashge3el3dif 13122* | A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif 13117, 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 13123* | An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (#‘𝑧) = 2} ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2sspr 13124* | 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 | elss2prOLD 13125* | An element of the set of subsets with two elements is an unordered pair. (Contributed by Alexander van der Vekens, 12-Jul-2018.) Obsolete version of elss2prb 13123 as of 1-Nov-2020. (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (#‘𝑧) = 2} → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑃 = {𝑥, 𝑦}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | exprelprel 13126* | 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 13127* | A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ (#‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1to3 13128* | 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 | fundmge2nop0 13129 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop 13130 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see isstruct 15705. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (#‘dom 𝐺)) → ¬ 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fundmge2nop 13130 | 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 13131 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop 13132 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see isstruct 15705. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → ¬ 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fun2dmnop 13132 | 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 | brfi1indlem 13133 | Lemma for brfi1ind 13136: The size of a set is the size of this set with one element removed, increased by 1. (Contributed by Alexander van der Vekens, 7-Jan-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) → ((#‘𝑉) = (𝑌 + 1) → (#‘(𝑉 ∖ {𝑁})) = 𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fi1uzind 13134* | 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 orderd pairs of vertices and edges) with a finite number of vertices, usually with 𝐿 = 0 (see opfi1ind 13139) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (#‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (#‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1uzind 13135* | 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 13136) 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 13136* | Properties of a binary relation with a finite first component, 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, e.g. usgrafis 25944. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel 𝐺 & ⊢ 𝐹 ∈ V & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (#‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indALT 13137* | Alternate proof of brfi1ind 13136, which does not use brfi1uzind 13135. (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 13138* | 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 orderd pairs of vertices and edges) with a finite number of vertices, usually with 𝐿 = 0 (see opfi1ind 13139) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (#‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((〈𝑉, 𝐸〉 ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (#‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1ind 13139* | 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 orderd pairs of vertices and edges) with a finite number of vertices, e.g. fusgrfis 40549. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (#‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((〈𝑉, 𝐸〉 ∈ 𝐺 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fi1uzindOLD 13140* | Obsolete version of fi1uzind 13134 as of 28-Mar-2021. (Contributed by AV, 22-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐹 ∈ 𝑈 & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (#‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (#‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1uzindOLD 13141* | Obsolete version of brfi1uzind 13135 as of 28-Mar-2021. (Contributed by AV, 7-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel 𝐺 & ⊢ 𝐹 ∈ 𝑈 & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (#‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (#‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indOLD 13142* | Obsolete version of brfi1ind 13136 as of 28-Mar-2021. (Contributed by AV, 7-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel 𝐺 & ⊢ 𝐹 ∈ 𝑈 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (#‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indALTOLD 13143* | Obsolete version of brfi1indALT 13137 as of 28-Mar-2021. (Contributed by AV, 7-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel 𝐺 & ⊢ 𝐹 ∈ 𝑈 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (#‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1uzindOLD 13144* | Obsolete version of opfi1uzind 13138 as of 28-Mar-2021. (Contributed by AV, 22-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 ∈ 𝑌 & ⊢ 𝐹 ∈ 𝑈 & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (#‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (#‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((〈𝑉, 𝐸〉 ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (#‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1indOLD 13145* | Obsolete version of opfi1ind 13139 as of 28-Mar-2021. (Contributed by AV, 22-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 ∈ 𝑌 & ⊢ 𝐹 ∈ 𝑈 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (#‘𝑣) = 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 is nonempty, finite and not a proper class, these restrictions are not made in the current definition df-word 13154, see, for example, s1cli 13237: 〈“𝐴”〉 ∈ Word V. Note that the empty word ∅ (i.e. the empty set) is the only word over an empty alphabet, see 0wrd0 13186. Besides the definition of words themselves, several operations on words are defined in this section:
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cword 13146 | Syntax for the Word operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class Word 𝑆 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | clsw 13147 | Extend class notation with the Last Symbol of a word. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class lastS | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cconcat 13148 | Syntax for the concatenation operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class ++ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cs1 13149 | Syntax for the singleton word constructor. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class 〈“𝐴”〉 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | csubstr 13150 | Syntax for the subword operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class substr | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | csplice 13151 | Syntax for the word splicing operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class splice | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | creverse 13152 | Syntax for the word reverse operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class reverse | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | creps 13153 | Extend class notation with words consisting of one repeated symbol. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class repeatS | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-word 13154* | Define the class of words over a set. A word (or 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 so that two words with the same symbols in the same order will be the same. This is sometimes denoted with the Kleene star, although properly speaking that is an operator on languages. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-lsw 13155 | 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))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-concat 13156* | Define the concatenation operator which combines two words. Definition in section 9.1 of [AhoHopUll] p. 318. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((#‘𝑠) + (#‘𝑡))) ↦ if(𝑥 ∈ (0..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-s1 13157 | Define the canonical injection from symbols to words. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-substr 13158* | Define an operation which extracts portions of words. Definition in section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ substr = (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st ‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))), ∅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-splice 13159* | Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr 〈0, (1st ‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd ‘(1st ‘𝑏)), (#‘𝑠)〉))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-reverse 13160* | Define an operation which reverses the order of symbols in a word. (Contributed by Stefan O'Rear, 26-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ reverse = (𝑠 ∈ V ↦ (𝑥 ∈ (0..^(#‘𝑠)) ↦ (𝑠‘(((#‘𝑠) − 1) − 𝑥)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-reps 13161* | Definition to construct a word consisting of one repeated symbol, often called "repeated symbol word" for short in the following. (Contributed by Alexander van der Vekens, 4-Nov-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ repeatS = (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrd 13162* | Property of being a word over a set with a 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 13163* | 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 (𝑆 ↑𝑚 (0..^𝑙))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrdi 13164 | 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 13165 | A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(#‘𝑊))⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrdb 13166 | A word over an alphabet is a function of 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 13167 | 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 13168 | 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 13169 | 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 13170 | The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdexb 13171 | 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 13172 | The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ V ⇒ ⊢ Word 𝑆 ∈ V | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdsymbcl 13173 | 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 13174 | 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 13175 | A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdlndm 13176 | The length of a word is not in the domain of the word (regarded as function). (Contributed by AV, 3-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∉ dom 𝑊) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrdsymb 13177* | 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 13178 | 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 13179 | 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 13180 | The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈ ℕ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdffz 13181 | A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((#‘𝑊) − 1))⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdeq 13182 | Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdeqi 13183 | Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 = 𝑇 ⇒ ⊢ Word 𝑆 = Word 𝑇 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrddm0 13184 | A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrd0 13185 | 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 13186 | The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ffz0iswrd 13187 | A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊:(0...𝐿)⟶𝑆 → 𝑊 ∈ Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nfwrd 13188 | Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Ⅎ𝑥𝑆 ⇒ ⊢ Ⅎ𝑥Word 𝑆 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | csbwrdg 13189* | Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdnval 13190* | Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Proof shortened by AV, 13-May-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 𝑁} = (𝑉 ↑𝑚 (0..^𝑁))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdmap 13191 | Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑𝑚 (0..^𝑁)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashwrdn 13192* | 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 13193* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 𝑁} ∈ Fin) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdsymb0 13194 | 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 13195 | A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (#‘𝑊))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdlenge2n0 13196 | 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 13197 | 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 13198* | 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 13199 | 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 13200 | 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) ∈ 𝑉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |