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