Home | Metamath
Proof Explorer Theorem List (p. 138 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 | hashf 13701 | The size function maps all finite sets to their cardinality, as members of ℕ0, and infinite sets to +∞. TODO-AV: mark as OBSOLETE and replace it by hashfxnn0 13700? (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 13-Jul-2014.) (Proof shortened by AV, 24-Oct-2021.) |
⊢ ♯:V⟶(ℕ0 ∪ {+∞}) | ||
Theorem | hashxnn0 13702 | The value of the hash function for a set is an extended nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Dec-2020.) |
⊢ (𝑀 ∈ 𝑉 → (♯‘𝑀) ∈ ℕ0*) | ||
Theorem | hashresfn 13703 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (♯ ↾ 𝐴) Fn 𝐴 | ||
Theorem | dmhashres 13704 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 12-Jan-2017.) |
⊢ dom (♯ ↾ 𝐴) = 𝐴 | ||
Theorem | hashnn0pnf 13705 | The value of the hash function for a set is either a nonnegative integer or positive infinity. TODO-AV: mark as OBSOLETE and replace it by hashxnn0 13702? (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ (𝑀 ∈ 𝑉 → ((♯‘𝑀) ∈ ℕ0 ∨ (♯‘𝑀) = +∞)) | ||
Theorem | hashnnn0genn0 13706 | If the size of a set is not a nonnegative integer, it is greater than or equal to any nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ ((𝑀 ∈ 𝑉 ∧ (♯‘𝑀) ∉ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ≤ (♯‘𝑀)) | ||
Theorem | hashnemnf 13707 | The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ≠ -∞) | ||
Theorem | hashv01gt1 13708 | The size of a set is either 0 or 1 or greater than 1. (Contributed by Alexander van der Vekens, 29-Dec-2017.) |
⊢ (𝑀 ∈ 𝑉 → ((♯‘𝑀) = 0 ∨ (♯‘𝑀) = 1 ∨ 1 < (♯‘𝑀))) | ||
Theorem | hashfz1 13709 | The set (1...𝑁) has 𝑁 elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁) | ||
Theorem | hashen 13710 | Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) ↔ 𝐴 ≈ 𝐵)) | ||
Theorem | hasheni 13711 | Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → (♯‘𝐴) = (♯‘𝐵)) | ||
Theorem | hasheqf1o 13712* | The size of two finite sets is equal if and only if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 17-Dec-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) | ||
Theorem | fiinfnf1o 13713* | There is no bijection between a finite set and an infinite set. (Contributed by Alexander van der Vekens, 25-Dec-2017.) |
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ¬ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) | ||
Theorem | focdmex 13714 | The codomain of an onto function is a set if its domain is a set. (Contributed by AV, 4-May-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ V) | ||
Theorem | hasheqf1oi 13715* | The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 25-Dec-2017.) (Revised by AV, 4-May-2021.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵))) | ||
Theorem | hashf1rn 13716 | The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 4-May-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (♯‘𝐹) = (♯‘ran 𝐹)) | ||
Theorem | hasheqf1od 13717 | The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by AV, 4-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) ⇒ ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵)) | ||
Theorem | fz1eqb 13718 | Two possibly-empty 1-based finite sets of sequential integers are equal iff their endpoints are equal. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 29-Mar-2014.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((1...𝑀) = (1...𝑁) ↔ 𝑀 = 𝑁)) | ||
Theorem | hashcard 13719 | The size function of the cardinality function. (Contributed by Mario Carneiro, 19-Sep-2013.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ (𝐴 ∈ Fin → (♯‘(card‘𝐴)) = (♯‘𝐴)) | ||
Theorem | hashcl 13720 | Closure of the ♯ function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.) |
⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0) | ||
Theorem | hashxrcl 13721 | Extended real closure of the ♯ function. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈ ℝ*) | ||
Theorem | hashclb 13722 | Reverse closure of the ♯ function. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ (♯‘𝐴) ∈ ℕ0)) | ||
Theorem | nfile 13723 | The size of any infinite set is always greater than or equal to the size of any set. (Contributed by AV, 13-Nov-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ (♯‘𝐵)) | ||
Theorem | hashvnfin 13724 | A set of finite size is a finite set. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((♯‘𝑆) = 𝑁 → 𝑆 ∈ Fin)) | ||
Theorem | hashnfinnn0 13725 | The size of an infinite set is not a nonnegative integer. (Contributed by Alexander van der Vekens, 21-Dec-2017.) (Proof shortened by Alexander van der Vekens, 18-Jan-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) ∉ ℕ0) | ||
Theorem | isfinite4 13726 | A finite set is equinumerous to the range of integers from one up to the hash value of the set. In other words, counting objects with natural numbers works if and only if it is a finite collection. (Contributed by Richard Penner, 26-Feb-2020.) |
⊢ (𝐴 ∈ Fin ↔ (1...(♯‘𝐴)) ≈ 𝐴) | ||
Theorem | hasheq0 13727 | Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) | ||
Theorem | hashneq0 13728 | Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ (𝐴 ∈ 𝑉 → (0 < (♯‘𝐴) ↔ 𝐴 ≠ ∅)) | ||
Theorem | hashgt0n0 13729 | If the size of a set is greater than 0, the set is not empty. (Contributed by AV, 5-Aug-2018.) (Proof shortened by AV, 18-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 0 < (♯‘𝐴)) → 𝐴 ≠ ∅) | ||
Theorem | hashnncl 13730 | Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) | ||
Theorem | hash0 13731 | The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.) |
⊢ (♯‘∅) = 0 | ||
Theorem | hashelne0d 13732 | A set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ¬ (♯‘𝐴) = 0) | ||
Theorem | hashsng 13733 | The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1) | ||
Theorem | hashen1 13734 | A set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 1 ↔ 𝐴 ≈ 1o)) | ||
Theorem | hash1elsn 13735 | A set of size 1 with a known element is the singleton of that element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → (♯‘𝐴) = 1) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 = {𝐵}) | ||
Theorem | hashrabrsn 13736* | The size of a restricted class abstraction restricted to a singleton is a nonnegative integer. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |
⊢ (♯‘{𝑥 ∈ {𝐴} ∣ 𝜑}) ∈ ℕ0 | ||
Theorem | hashrabsn01 13737* | The size of a restricted class abstraction restricted to a singleton is either 0 or 1. (Contributed by Alexander van der Vekens, 3-Sep-2018.) |
⊢ ((♯‘{𝑥 ∈ {𝐴} ∣ 𝜑}) = 𝑁 → (𝑁 = 0 ∨ 𝑁 = 1)) | ||
Theorem | hashrabsn1 13738* | If the size of a restricted class abstraction restricted to a singleton is 1, the condition of the class abstraction must hold for the singleton. (Contributed by Alexander van der Vekens, 3-Sep-2018.) |
⊢ ((♯‘{𝑥 ∈ {𝐴} ∣ 𝜑}) = 1 → [𝐴 / 𝑥]𝜑) | ||
Theorem | hashfn 13739 | A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ (𝐹 Fn 𝐴 → (♯‘𝐹) = (♯‘𝐴)) | ||
Theorem | fseq1hash 13740 | The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (♯‘𝐹) = 𝑁) | ||
Theorem | hashgadd 13741 | 𝐺 maps ordinal addition to integer addition. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐺‘(𝐴 +o 𝐵)) = ((𝐺‘𝐴) + (𝐺‘𝐵))) | ||
Theorem | hashgval2 13742 | A short expression for the 𝐺 function of hashgf1o 13342. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ (♯ ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) | ||
Theorem | hashdom 13743 | Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵)) | ||
Theorem | hashdomi 13744 | Non-strict order relation of the ♯ function on the full cardinal poset. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ (𝐴 ≼ 𝐵 → (♯‘𝐴) ≤ (♯‘𝐵)) | ||
Theorem | hashsdom 13745 | Strict dominance relation for the size function. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) < (♯‘𝐵) ↔ 𝐴 ≺ 𝐵)) | ||
Theorem | hashun 13746 | The size of the union of disjoint finite sets is the sum of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) | ||
Theorem | hashun2 13747 | The size of the union of finite sets is less than or equal to the sum of their sizes. (Contributed by Mario Carneiro, 23-Sep-2013.) (Proof shortened by Mario Carneiro, 27-Jul-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ∪ 𝐵)) ≤ ((♯‘𝐴) + (♯‘𝐵))) | ||
Theorem | hashun3 13748 | The size of the union of finite sets is the sum of their sizes minus the size of the intersection. (Contributed by Mario Carneiro, 6-Aug-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ∪ 𝐵)) = (((♯‘𝐴) + (♯‘𝐵)) − (♯‘(𝐴 ∩ 𝐵)))) | ||
Theorem | hashinfxadd 13749 | The extended real addition of the size of an infinite set with the size of an arbitrary set yields plus infinity. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (♯‘𝐴) ∉ ℕ0) → ((♯‘𝐴) +𝑒 (♯‘𝐵)) = +∞) | ||
Theorem | hashunx 13750 | The size of the union of disjoint sets is the result of the extended real addition of their sizes, analogous to hashun 13746. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵))) | ||
Theorem | hashge0 13751 | The cardinality of a set is greater than or equal to zero. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ (𝐴 ∈ 𝑉 → 0 ≤ (♯‘𝐴)) | ||
Theorem | hashgt0 13752 | The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 0 < (♯‘𝐴)) | ||
Theorem | hashge1 13753 | The cardinality of a nonempty set is greater than or equal to one. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 1 ≤ (♯‘𝐴)) | ||
Theorem | 1elfz0hash 13754 | 1 is an element of the finite set of sequential nonnegative integers bounded by the size of a nonempty finite set. (Contributed by AV, 9-May-2020.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → 1 ∈ (0...(♯‘𝐴))) | ||
Theorem | hashnn0n0nn 13755 | If a nonnegative integer is the size of a set which contains at least one element, this integer is a positive integer. (Contributed by Alexander van der Vekens, 9-Jan-2018.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0) ∧ ((♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉)) → 𝑌 ∈ ℕ) | ||
Theorem | hashunsng 13756 | The size of the union of a finite set with a disjoint singleton is one more than the size of the set. (Contributed by Paul Chapman, 30-Nov-2012.) |
⊢ (𝐵 ∈ 𝑉 → ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴) → (♯‘(𝐴 ∪ {𝐵})) = ((♯‘𝐴) + 1))) | ||
Theorem | hashunsngx 13757 | The size of the union of a set with a disjoint singleton is the extended real addition of the size of the set and 1, analogous to hashunsng 13756. (Contributed by BTernaryTau, 9-Sep-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝐵 ∈ 𝐴 → (♯‘(𝐴 ∪ {𝐵})) = ((♯‘𝐴) +𝑒 1))) | ||
Theorem | hashunsnggt 13758 | The size of a set is greater than a nonnegative integer N if and only if the size of the union of that set with a disjoint singleton is greater than N + 1. (Contributed by BTernaryTau, 10-Sep-2023.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑁 ∈ ℕ0) ∧ ¬ 𝐵 ∈ 𝐴) → (𝑁 < (♯‘𝐴) ↔ (𝑁 + 1) < (♯‘(𝐴 ∪ {𝐵})))) | ||
Theorem | hashprg 13759 | The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Revised by AV, 18-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2)) | ||
Theorem | elprchashprn2 13760 | If one element of an unordered pair is not a set, the size of the unordered pair is not 2. (Contributed by Alexander van der Vekens, 7-Oct-2017.) |
⊢ (¬ 𝑀 ∈ V → ¬ (♯‘{𝑀, 𝑁}) = 2) | ||
Theorem | hashprb 13761 | The size of an unordered pair is 2 if and only if its elements are different sets. (Contributed by Alexander van der Vekens, 17-Jan-2018.) |
⊢ ((𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁) ↔ (♯‘{𝑀, 𝑁}) = 2) | ||
Theorem | hashprdifel 13762 | The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} ⇒ ⊢ ((♯‘𝑆) = 2 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | prhash2ex 13763 | There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 13772, numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020.) |
⊢ (♯‘{0, 1}) = 2 | ||
Theorem | hashle00 13764 | If the size of a set is less than or equal to zero, the set must be empty. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Proof shortened by AV, 24-Oct-2021.) |
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) ≤ 0 ↔ 𝑉 = ∅)) | ||
Theorem | hashgt0elex 13765* | If the size of a set is greater than zero, then the set must contain at least one element. (Contributed by Alexander van der Vekens, 6-Jan-2018.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 0 < (♯‘𝑉)) → ∃𝑥 𝑥 ∈ 𝑉) | ||
Theorem | hashgt0elexb 13766* | The size of a set is greater than zero if and only if the set contains at least one element. (Contributed by Alexander van der Vekens, 18-Jan-2018.) |
⊢ (𝑉 ∈ 𝑊 → (0 < (♯‘𝑉) ↔ ∃𝑥 𝑥 ∈ 𝑉)) | ||
Theorem | hashp1i 13767 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 = suc 𝐴 & ⊢ (♯‘𝐴) = 𝑀 & ⊢ (𝑀 + 1) = 𝑁 ⇒ ⊢ (♯‘𝐵) = 𝑁 | ||
Theorem | hash1 13768 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (♯‘1o) = 1 | ||
Theorem | hash2 13769 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (♯‘2o) = 2 | ||
Theorem | hash3 13770 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (♯‘3o) = 3 | ||
Theorem | hash4 13771 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (♯‘4o) = 4 | ||
Theorem | pr0hash2ex 13772 | There is (at least) one set with two different elements: the unordered pair containing the empty set and the singleton containing the empty set. (Contributed by AV, 29-Jan-2020.) |
⊢ (♯‘{∅, {∅}}) = 2 | ||
Theorem | hashss 13773 | The size of a subset is less than or equal to the size of its superset. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (♯‘𝐵) ≤ (♯‘𝐴)) | ||
Theorem | prsshashgt1 13774 | The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (♯‘𝐶))) | ||
Theorem | hashin 13775 | The size of the intersection of a set and a class is less than or equal to the size of the set. (Contributed by AV, 4-Jan-2021.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘(𝐴 ∩ 𝐵)) ≤ (♯‘𝐴)) | ||
Theorem | hashssdif 13776 | The size of the difference of a finite set and a subset is the set's size minus the subset's. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘(𝐴 ∖ 𝐵)) = ((♯‘𝐴) − (♯‘𝐵))) | ||
Theorem | hashdif 13777 | The size of the difference of a finite set and another set is the first set's size minus that of the intersection of both. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
⊢ (𝐴 ∈ Fin → (♯‘(𝐴 ∖ 𝐵)) = ((♯‘𝐴) − (♯‘(𝐴 ∩ 𝐵)))) | ||
Theorem | hashdifsn 13778 | The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (♯‘(𝐴 ∖ {𝐵})) = ((♯‘𝐴) − 1)) | ||
Theorem | hashdifpr 13779 | The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.) |
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (♯‘(𝐴 ∖ {𝐵, 𝐶})) = ((♯‘𝐴) − 2)) | ||
Theorem | hashsn01 13780 | The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021.) |
⊢ ((♯‘{𝐴}) = 0 ∨ (♯‘{𝐴}) = 1) | ||
Theorem | hashsnle1 13781 | The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021.) |
⊢ (♯‘{𝐴}) ≤ 1 | ||
Theorem | hashsnlei 13782 | Get an upper bound on a concretely specified finite set. Base case: singleton set. (Contributed by Mario Carneiro, 11-Feb-2015.) (Proof shortened by AV, 23-Feb-2021.) |
⊢ ({𝐴} ∈ Fin ∧ (♯‘{𝐴}) ≤ 1) | ||
Theorem | hash1snb 13783* | The size of a set is 1 if and only if it is a singleton (containing a set). (Contributed by Alexander van der Vekens, 7-Dec-2017.) |
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 ↔ ∃𝑎 𝑉 = {𝑎})) | ||
Theorem | euhash1 13784* | The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.) |
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 ↔ ∃!𝑎 𝑎 ∈ 𝑉)) | ||
Theorem | hash1n0 13785 | If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) = 1) → 𝐴 ≠ ∅) | ||
Theorem | hashgt12el 13786* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑎 ≠ 𝑏) | ||
Theorem | hashgt12el2 13787* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏) | ||
Theorem | hashgt23el 13788* | A set with more than two elements has at least three different elements. (Contributed by BTernaryTau, 21-Sep-2023.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | ||
Theorem | hashunlei 13789 | Get an upper bound on a concretely specified finite set. Induction step: union of two finite bounded sets. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐶 = (𝐴 ∪ 𝐵) & ⊢ (𝐴 ∈ Fin ∧ (♯‘𝐴) ≤ 𝐾) & ⊢ (𝐵 ∈ Fin ∧ (♯‘𝐵) ≤ 𝑀) & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ (𝐾 + 𝑀) = 𝑁 ⇒ ⊢ (𝐶 ∈ Fin ∧ (♯‘𝐶) ≤ 𝑁) | ||
Theorem | hashsslei 13790 | Get an upper bound on a concretely specified finite set. Transfer boundedness to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝐴 ∈ Fin ∧ (♯‘𝐴) ≤ 𝑁) & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝐵 ∈ Fin ∧ (♯‘𝐵) ≤ 𝑁) | ||
Theorem | hashfz 13791 | Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario Carneiro, 15-Apr-2015.) |
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘(𝐴...𝐵)) = ((𝐵 − 𝐴) + 1)) | ||
Theorem | fzsdom2 13792 | Condition for finite ranges to have a strict dominance relation. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Revised by Mario Carneiro, 15-Apr-2015.) |
⊢ (((𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐶 ∈ ℤ) ∧ 𝐵 < 𝐶) → (𝐴...𝐵) ≺ (𝐴...𝐶)) | ||
Theorem | hashfzo 13793 | Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘(𝐴..^𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | hashfzo0 13794 | Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐵 ∈ ℕ0 → (♯‘(0..^𝐵)) = 𝐵) | ||
Theorem | hashfzp1 13795 | Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.) |
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | hashfz0 13796 | Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ (𝐵 ∈ ℕ0 → (♯‘(0...𝐵)) = (𝐵 + 1)) | ||
Theorem | hashxplem 13797 | Lemma for hashxp 13798. (Contributed by Paul Chapman, 30-Nov-2012.) |
⊢ 𝐵 ∈ Fin ⇒ ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) | ||
Theorem | hashxp 13798 | The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) | ||
Theorem | hashmap 13799 | The size of the set exponential of two finite sets is the exponential of their sizes. (This is the original motivation behind the notation for set exponentiation.) (Contributed by Mario Carneiro, 5-Aug-2014.) (Proof shortened by AV, 18-Jul-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ↑m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵))) | ||
Theorem | hashpw 13800 | The size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by Paul Chapman, 30-Nov-2012.) (Proof shortened by Mario Carneiro, 5-Aug-2014.) |
⊢ (𝐴 ∈ Fin → (♯‘𝒫 𝐴) = (2↑(♯‘𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |