Home | Metamath
Proof Explorer Theorem List (p. 139 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfun 13801 | A finite set is a function iff it is equinumerous to its domain. (Contributed by Mario Carneiro, 26-Sep-2013.) (Revised by Mario Carneiro, 12-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashres 13802 | The number of elements of a finite function restricted to a subset of its domain is equal to the number of elements of that subset. (Contributed by AV, 15-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴) → (♯‘(𝐴 ↾ 𝐵)) = (♯‘𝐵)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashreshashfun 13803 | The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴) → (♯‘𝐴) = ((♯‘(𝐴 ↾ 𝐵)) + (♯‘(dom 𝐴 ∖ 𝐵)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashimarn 13804 | The size of the image of a one-to-one function 𝐸 under the range of a function 𝐹 which is a one-to-one function into the domain of 𝐸 equals the size of the function 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) (Proof shortened by AV, 4-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) → (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → (♯‘(𝐸 “ ran 𝐹)) = (♯‘𝐹))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashimarni 13805 | If the size of the image of a one-to-one function 𝐸 under the range of a function 𝐹 which is a one-to-one function into the domain of 𝐸 is a nonnegative integer, the size of the function 𝐹 is the same nonnegative integer. (Contributed by Alexander van der Vekens, 4-Feb-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) → ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 ∧ 𝑃 = (𝐸 “ ran 𝐹) ∧ (♯‘𝑃) = 𝑁) → (♯‘𝐹) = 𝑁)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | resunimafz0 13806 | TODO-AV: Revise using 𝐹 ∈ Word dom 𝐼? Formerly part of proof of eupth2lem3 28017: The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) ⇒ ⊢ (𝜑 → (𝐼 ↾ (𝐹 “ (0...𝑁))) = ((𝐼 ↾ (𝐹 “ (0..^𝑁))) ∪ {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfz0hash 13807 | The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (0...𝑁)) → (♯‘𝐹) = (𝑁 + 1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ffz0hash 13808 | The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV, 11-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶𝐵) → (♯‘𝐹) = (𝑁 + 1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfz0hashnn0 13809 | The size of a function on a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐹 Fn (0...𝑁) → (♯‘𝐹) ∈ ℕ0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ffzo0hash 13810 | The size of a function on a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 25-Mar-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (0..^𝑁)) → (♯‘𝐹) = 𝑁) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfzo0hash 13811 | The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0..^𝑁)⟶𝐵) → (♯‘𝐹) = 𝑁) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfzo0hashnn0 13812 | The value of the size function on a half-open range of nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐹 Fn (0..^𝑁) → (♯‘𝐹) ∈ ℕ0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashbclem 13813* | Lemma for hashbc 13814: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗})) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashbc 13814* | 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 13815* | The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1lem1 13816* | Lemma for hashf1 13818. (Contributed by Mario Carneiro, 17-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵)) & ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) ⇒ ⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝐹)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1lem2 13817* | Lemma for hashf1 13818. (Contributed by Mario Carneiro, 17-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵)) ⇒ ⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1 13818* | 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 13819* | 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 13820 | Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ≤ (𝐴, 𝐵))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | leisorel 13821 | Version of isorel 7081 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1isolem 13822* | Lemma for fz1iso 13823. (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) & ⊢ 𝐵 = (ℕ ∩ (◡ < “ {((♯‘𝐴) + 1)})) & ⊢ 𝐶 = (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1iso 13823* | 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 13824* | Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 8733. (Contributed by Thierry Arnoux, 5-Jul-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ℕ ∃𝑥 ∈ 𝒫 𝐴(♯‘𝑥) = 𝑛) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | seqcoll 13825* | 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 13826* | 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 13827 | Corollary of the Pigeonhole Principle using equality. Equivalent of phpeqd 8708 expressed using the hash function. (Contributed by Rohan Ridenour, 3-Aug-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | phphashrd 13828 | Corollary of the Pigeonhole Principle using equality. Equivalent of phphashd 13827 with reversed arguments. (Contributed by Rohan Ridenour, 3-Aug-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashprlei 13829 | An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({𝐴, 𝐵} ∈ Fin ∧ (♯‘{𝐴, 𝐵}) ≤ 2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2pr 13830* | A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 2) → ∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prde 13831* | 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 13832* | 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 13833* | A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 2 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | prprrab 13834 | 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 13835 | The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝑃 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prd 13836 | 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 13837 | 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 13838* | 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 13839* | 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 13840* | 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 13841* | A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐷 ∈ 𝑉 ∧ 2 ≤ (♯‘𝐷)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difr 13842* | A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐷 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) → 2 ≤ (♯‘𝐷)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difb 13843* | A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐷 ∈ 𝑉 → (2 ≤ (♯‘𝐷) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashdmpropge2 13844 | 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 13845 | An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({𝐴, 𝐵, 𝐶} ∈ Fin ∧ (♯‘{𝐴, 𝐵, 𝐶}) ≤ 3) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashtpg 13846 | 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 13847* | A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif 13841, 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 13848* | An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (♯‘𝑧) = 2} ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2sspr 13849* | 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 13850* | 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 13851* | A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1to3 13852* | 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 13853 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop 13854 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see structn0fun 16497. (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 13854 | 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 13855 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop 13856 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see structn0fun 16497. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → ¬ 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fun2dmnop 13856 | 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 13857 | 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 13858* | 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 13863) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (♯‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1uzind 13859* | 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 13860) 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 13860* | 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 13861* | Alternate proof of brfi1ind 13860, which does not use brfi1uzind 13859. (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 13862* | 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 13863) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((〈𝑉, 𝐸〉 ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1ind 13863* | 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 27114. (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 13865, see, for example, s1cli 13961: 〈“𝐴”〉 ∈ Word V. Note that the empty word ∅ (i.e. the empty set) is the only word over an empty alphabet, see 0wrd0 13892. 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 13864 | Syntax for the Word operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class Word 𝑆 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-word 13865* | 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 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word (see frmdval 18018). (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 13866* | 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 13867* | 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 13868 | 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 13869 | A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrdb 13870 | 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 13871 | 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 13872 | 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 13873 | 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 13874 | 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 | wrdexgOLD 13875 | Obsolete proof of wrdexg 13874 as of 29-Apr-2023. (Contributed by Mario Carneiro, 26-Feb-2016.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdexb 13876 | 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 13877 | The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ V ⇒ ⊢ Word 𝑆 ∈ V | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdsymbcl 13878 | 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 13879 | 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 13880 | 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 13881 | 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 | wrdlndmOLD 13882 | Obsolete proof of wrdlndm 13881 as of 1-May-2023. (Contributed by AV, 3-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∉ dom 𝑊) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrdsymb 13883* | 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 13884 | 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 13885 | 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 13886 | The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdffz 13887 | A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdeq 13888 | Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdeqi 13889 | Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 = 𝑇 ⇒ ⊢ Word 𝑆 = Word 𝑇 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrddm0 13890 | A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrd0 13891 | 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 13892 | The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ffz0iswrd 13893 | 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 | ffz0iswrdOLD 13894 | Obsolete proof of ffz0iswrd 13893 as of 1-May-2023. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑊:(0...𝐿)⟶𝑆 → 𝑊 ∈ Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdsymb 13895 | A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nfwrd 13896 | Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Ⅎ𝑥𝑆 ⇒ ⊢ Ⅎ𝑥Word 𝑆 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | csbwrdg 13897* | Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdnval 13898* | 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 13899 | Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑m (0..^𝑁)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashwrdn 13900* | 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 𝑉 ∣ (♯‘𝑤) = 𝑁}) = ((♯‘𝑉)↑𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |