Home | Metamath
Proof Explorer Theorem List (p. 143 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hashrabsn01 14201* | 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 14202* | 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 14203 | A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.) |
โข (๐น Fn ๐ด โ (โฏโ๐น) = (โฏโ๐ด)) | ||
Theorem | fseq1hash 14204 | 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 14205 | ๐บ 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 14206 | A short expression for the ๐บ function of hashgf1o 13805. (Contributed by Mario Carneiro, 24-Jan-2015.) |
โข (โฏ โพ ฯ) = (rec((๐ฅ โ V โฆ (๐ฅ + 1)), 0) โพ ฯ) | ||
Theorem | hashdom 14207 | Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.) |
โข ((๐ด โ Fin โง ๐ต โ ๐) โ ((โฏโ๐ด) โค (โฏโ๐ต) โ ๐ด โผ ๐ต)) | ||
Theorem | hashdomi 14208 | Non-strict order relation of the โฏ function on the full cardinal poset. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
โข (๐ด โผ ๐ต โ (โฏโ๐ด) โค (โฏโ๐ต)) | ||
Theorem | hashsdom 14209 | Strict dominance relation for the size function. (Contributed by Mario Carneiro, 18-Aug-2014.) |
โข ((๐ด โ Fin โง ๐ต โ Fin) โ ((โฏโ๐ด) < (โฏโ๐ต) โ ๐ด โบ ๐ต)) | ||
Theorem | hashun 14210 | 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 14211 | 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 14212 | 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 14213 | 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 14214 | The size of the union of disjoint sets is the result of the extended real addition of their sizes, analogous to hashun 14210. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐ โง (๐ด โฉ ๐ต) = โ ) โ (โฏโ(๐ด โช ๐ต)) = ((โฏโ๐ด) +๐ (โฏโ๐ต))) | ||
Theorem | hashge0 14215 | The cardinality of a set is greater than or equal to zero. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
โข (๐ด โ ๐ โ 0 โค (โฏโ๐ด)) | ||
Theorem | hashgt0 14216 | The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
โข ((๐ด โ ๐ โง ๐ด โ โ ) โ 0 < (โฏโ๐ด)) | ||
Theorem | hashge1 14217 | The cardinality of a nonempty set is greater than or equal to one. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
โข ((๐ด โ ๐ โง ๐ด โ โ ) โ 1 โค (โฏโ๐ด)) | ||
Theorem | 1elfz0hash 14218 | 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 14219 | 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 14220 | 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 14221 | 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 14220. (Contributed by BTernaryTau, 9-Sep-2023.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (ยฌ ๐ต โ ๐ด โ (โฏโ(๐ด โช {๐ต})) = ((โฏโ๐ด) +๐ 1))) | ||
Theorem | hashunsnggt 14222 | 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 14223 | 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 14224 | 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 14225 | 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 14226 | The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020.) |
โข ๐ = {๐ด, ๐ต} โ โข ((โฏโ๐) = 2 โ (๐ด โ ๐ โง ๐ต โ ๐ โง ๐ด โ ๐ต)) | ||
Theorem | prhash2ex 14227 | There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 14236, 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 14228 | 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 14229* | 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 14230* | 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 14231 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
โข ๐ด โ ฯ & โข ๐ต = suc ๐ด & โข (โฏโ๐ด) = ๐ & โข (๐ + 1) = ๐ โ โข (โฏโ๐ต) = ๐ | ||
Theorem | hash1 14232 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
โข (โฏโ1o) = 1 | ||
Theorem | hash2 14233 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
โข (โฏโ2o) = 2 | ||
Theorem | hash3 14234 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
โข (โฏโ3o) = 3 | ||
Theorem | hash4 14235 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
โข (โฏโ4o) = 4 | ||
Theorem | pr0hash2ex 14236 | 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 14237 | 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 14238 | The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.) |
โข (((๐ด โ ๐ โง ๐ต โ ๐ โง ๐ด โ ๐ต) โง ๐ถ โ ๐) โ ({๐ด, ๐ต} โ ๐ถ โ 2 โค (โฏโ๐ถ))) | ||
Theorem | hashin 14239 | 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 14240 | 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 14241 | 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 14242 | 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 14243 | The size of the difference of a finite set and a proper pair of its elements is the set's size minus 2. (Contributed by AV, 16-Dec-2020.) |
โข ((๐ด โ Fin โง (๐ต โ ๐ด โง ๐ถ โ ๐ด โง ๐ต โ ๐ถ)) โ (โฏโ(๐ด โ {๐ต, ๐ถ})) = ((โฏโ๐ด) โ 2)) | ||
Theorem | hashsn01 14244 | The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021.) |
โข ((โฏโ{๐ด}) = 0 โจ (โฏโ{๐ด}) = 1) | ||
Theorem | hashsnle1 14245 | The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021.) |
โข (โฏโ{๐ด}) โค 1 | ||
Theorem | hashsnlei 14246 | 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 14247* | 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 14248* | The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.) |
โข (๐ โ ๐ โ ((โฏโ๐) = 1 โ โ!๐ ๐ โ ๐)) | ||
Theorem | hash1n0 14249 | If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.) |
โข ((๐ด โ ๐ โง (โฏโ๐ด) = 1) โ ๐ด โ โ ) | ||
Theorem | hashgt12el 14250* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
โข ((๐ โ ๐ โง 1 < (โฏโ๐)) โ โ๐ โ ๐ โ๐ โ ๐ ๐ โ ๐) | ||
Theorem | hashgt12el2 14251* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
โข ((๐ โ ๐ โง 1 < (โฏโ๐) โง ๐ด โ ๐) โ โ๐ โ ๐ ๐ด โ ๐) | ||
Theorem | hashgt23el 14252* | A set with more than two elements has at least three different elements. (Contributed by BTernaryTau, 21-Sep-2023.) |
โข ((๐ โ ๐ โง 2 < (โฏโ๐)) โ โ๐ โ ๐ โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) | ||
Theorem | hashunlei 14253 | 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 14254 | 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 14255 | 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 14256 | 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 14257 | Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
โข (๐ต โ (โคโฅโ๐ด) โ (โฏโ(๐ด..^๐ต)) = (๐ต โ ๐ด)) | ||
Theorem | hashfzo0 14258 | Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
โข (๐ต โ โ0 โ (โฏโ(0..^๐ต)) = ๐ต) | ||
Theorem | hashfzp1 14259 | Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.) |
โข (๐ต โ (โคโฅโ๐ด) โ (โฏโ((๐ด + 1)...๐ต)) = (๐ต โ ๐ด)) | ||
Theorem | hashfz0 14260 | 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 14261 | Lemma for hashxp 14262. (Contributed by Paul Chapman, 30-Nov-2012.) |
โข ๐ต โ Fin โ โข (๐ด โ Fin โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยท (โฏโ๐ต))) | ||
Theorem | hashxp 14262 | 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 14263 | 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 14264 | 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โ(โฏโ๐ด))) | ||
Theorem | hashfun 14265 | 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 14266 | 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 14267 | The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021.) |
โข ((Fun ๐ด โง ๐ด โ Fin โง ๐ต โ dom ๐ด) โ (โฏโ๐ด) = ((โฏโ(๐ด โพ ๐ต)) + (โฏโ(dom ๐ด โ ๐ต)))) | ||
Theorem | hashimarn 14268 | 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 14269 | 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 14270 | TODO-AV: Revise using ๐น โ Word dom ๐ผ? Formerly part of proof of eupth2lem3 28966: 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 14271 | 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 14272 | 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 14273 | 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 14274 | 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 14275 | 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 14276 | 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 14277* | Lemma for hashbc 14278: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ยฌ ๐ง โ ๐ด) & โข (๐ โ โ๐ โ โค ((โฏโ๐ด)C๐) = (โฏโ{๐ฅ โ ๐ซ ๐ด โฃ (โฏโ๐ฅ) = ๐})) & โข (๐ โ ๐พ โ โค) โ โข (๐ โ ((โฏโ(๐ด โช {๐ง}))C๐พ) = (โฏโ{๐ฅ โ ๐ซ (๐ด โช {๐ง}) โฃ (โฏโ๐ฅ) = ๐พ})) | ||
Theorem | hashbc 14278* | 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 14279* | The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by AV, 7-Aug-2024.) |
โข ((๐ด โ ๐ต โง ๐ถ โ ๐ท) โ {๐ โฃ ๐:๐ดโ1-1-ontoโ๐ถ} โ {๐ โฃ ๐:๐ตโ1-1-ontoโ๐ท}) | ||
Theorem | hashfacenOLD 14280* | Obsolete version of hashfacen 14279 as of 7-Aug-2024. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ((๐ด โ ๐ต โง ๐ถ โ ๐ท) โ {๐ โฃ ๐:๐ดโ1-1-ontoโ๐ถ} โ {๐ โฃ ๐:๐ตโ1-1-ontoโ๐ท}) | ||
Theorem | hashf1lem1 14281* | Lemma for hashf1 14284. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ยฌ ๐ง โ ๐ด) & โข (๐ โ ((โฏโ๐ด) + 1) โค (โฏโ๐ต)) & โข (๐ โ ๐น:๐ดโ1-1โ๐ต) โ โข (๐ โ {๐ โฃ ((๐ โพ ๐ด) = ๐น โง ๐:(๐ด โช {๐ง})โ1-1โ๐ต)} โ (๐ต โ ran ๐น)) | ||
Theorem | hashf1lem1OLD 14282* | Obsolete version of hashf1lem1 14281 as of 7-Aug-2024. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ยฌ ๐ง โ ๐ด) & โข (๐ โ ((โฏโ๐ด) + 1) โค (โฏโ๐ต)) & โข (๐ โ ๐น:๐ดโ1-1โ๐ต) โ โข (๐ โ {๐ โฃ ((๐ โพ ๐ด) = ๐น โง ๐:(๐ด โช {๐ง})โ1-1โ๐ต)} โ (๐ต โ ran ๐น)) | ||
Theorem | hashf1lem2 14283* | Lemma for hashf1 14284. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ยฌ ๐ง โ ๐ด) & โข (๐ โ ((โฏโ๐ด) + 1) โค (โฏโ๐ต)) โ โข (๐ โ (โฏโ{๐ โฃ ๐:(๐ด โช {๐ง})โ1-1โ๐ต}) = (((โฏโ๐ต) โ (โฏโ๐ด)) ยท (โฏโ{๐ โฃ ๐:๐ดโ1-1โ๐ต}))) | ||
Theorem | hashf1 14284* | 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 14285* | 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 14286 | Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐น Isom < , < (๐ด, ๐ต) โ ๐น Isom โค , โค (๐ด, ๐ต))) | ||
Theorem | leisorel 14287 | Version of isorel 7266 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.) |
โข ((๐น Isom < , < (๐ด, ๐ต) โง (๐ด โ โ* โง ๐ต โ โ*) โง (๐ถ โ ๐ด โง ๐ท โ ๐ด)) โ (๐ถ โค ๐ท โ (๐นโ๐ถ) โค (๐นโ๐ท))) | ||
Theorem | fz1isolem 14288* | Lemma for fz1iso 14289. (Contributed by Mario Carneiro, 2-Apr-2014.) |
โข ๐บ = (rec((๐ โ V โฆ (๐ + 1)), 1) โพ ฯ) & โข ๐ต = (โ โฉ (โก < โ {((โฏโ๐ด) + 1)})) & โข ๐ถ = (ฯ โฉ (โก๐บโ((โฏโ๐ด) + 1))) & โข ๐ = OrdIso(๐ , ๐ด) โ โข ((๐ Or ๐ด โง ๐ด โ Fin) โ โ๐ ๐ Isom < , ๐ ((1...(โฏโ๐ด)), ๐ด)) | ||
Theorem | fz1iso 14289* | 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 14290* | Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 9138. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
โข (ยฌ ๐ด โ Fin โ โ๐ โ โ โ๐ฅ โ ๐ซ ๐ด(โฏโ๐ฅ) = ๐) | ||
Theorem | seqcoll 14291* | 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 14292* | 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 14293 | Corollary of the Pigeonhole Principle using equality. Equivalent of phpeqd 9093 expressed using the hash function. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ ๐ด) & โข (๐ โ (โฏโ๐ด) = (โฏโ๐ต)) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | phphashrd 14294 | Corollary of the Pigeonhole Principle using equality. Equivalent of phphashd 14293 with reversed arguments. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ (โฏโ๐ด) = (โฏโ๐ต)) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | hashprlei 14295 | An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.) |
โข ({๐ด, ๐ต} โ Fin โง (โฏโ{๐ด, ๐ต}) โค 2) | ||
Theorem | hash2pr 14296* | A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
โข ((๐ โ ๐ โง (โฏโ๐) = 2) โ โ๐โ๐ ๐ = {๐, ๐}) | ||
Theorem | hash2prde 14297* | 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 14298* | 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 14299* | A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) |
โข (๐ โ ๐ โ ((โฏโ๐) = 2 โ โ๐ โ ๐ โ๐ โ ๐ (๐ โ ๐ โง ๐ = {๐, ๐}))) | ||
Theorem | prprrab 14300 | The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020.) |
โข {๐ฅ โ (๐ซ ๐ด โ {โ }) โฃ (โฏโ๐ฅ) = 2} = {๐ฅ โ ๐ซ ๐ด โฃ (โฏโ๐ฅ) = 2} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |