Home | Metamath
Proof Explorer Theorem List (p. 83 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | findcard2s 8201* | Variation of findcard2 8200 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.) |
Theorem | findcard2d 8202* | Deduction version of findcard2 8200. (Contributed by SO, 16-Jul-2018.) |
Theorem | findcard3 8203* | Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013.) |
Theorem | ac6sfi 8204* | A version of ac6s 9306 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
Theorem | frfi 8205 | A partial order is well-founded on a finite set. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
Theorem | fimax2g 8206* | A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
Theorem | fimaxg 8207* | A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
Theorem | fisupg 8208* | Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | wofi 8209 | A total order on a finite set is a well-order. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
Theorem | ordunifi 8210 | The maximum of a finite collection of ordinals is in the set. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 29-Jan-2014.) |
Theorem | nnunifi 8211 | The union (supremum) of a finite set of finite ordinals is a finite ordinal. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
Theorem | unblem1 8212* | Lemma for unbnn 8216. After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. (Contributed by NM, 3-Dec-2003.) |
Theorem | unblem2 8213* | Lemma for unbnn 8216. The value of the function belongs to the unbounded set of natural numbers . (Contributed by NM, 3-Dec-2003.) |
Theorem | unblem3 8214* | Lemma for unbnn 8216. The value of the function is less than its value at a successor. (Contributed by NM, 3-Dec-2003.) |
Theorem | unblem4 8215* | Lemma for unbnn 8216. The function maps the set of natural numbers one-to-one to the set of unbounded natural numbers . (Contributed by NM, 3-Dec-2003.) |
Theorem | unbnn 8216* | Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of [Suppes] p. 151. See unbnn3 8556 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003.) |
Theorem | unbnn2 8217* | Version of unbnn 8216 that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004.) |
Theorem | isfinite2 8218 | Any set strictly dominated by the class of natural numbers is finite. Sufficiency part of Theorem 42 of [Suppes] p. 151. This theorem does not require the Axiom of Infinity. (Contributed by NM, 24-Apr-2004.) |
Theorem | nnsdomg 8219 | Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 15-Jun-1998.) |
Theorem | isfiniteg 8220 | A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of [Suppes] p. 151. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 3-Nov-2002.) (Revised by Mario Carneiro, 27-Apr-2015.) |
Theorem | infsdomnn 8221 | An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
Theorem | infn0 8222 | An infinite set is not empty. (Contributed by NM, 23-Oct-2004.) |
Theorem | fin2inf 8223 | This (useless) theorem, which was proved without the Axiom of Infinity, demonstrates an artifact of our definition of binary relation, which is meaningful only when its arguments exist. In particular, the antecedent cannot be satisfied unless exists. (Contributed by NM, 13-Nov-2003.) |
Theorem | unfilem1 8224* | Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | unfilem2 8225* | Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | unfilem3 8226 | Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 16-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | unfi 8227 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.) |
Theorem | unfir 8228 | If a union is finite, the operands are finite. Converse of unfi 8227. (Contributed by FL, 3-Aug-2009.) |
Theorem | unfi2 8229 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 8227 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 8223). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
Theorem | difinf 8230 | An infinite set minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.) |
Theorem | xpfi 8231 | The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) |
Theorem | 3xpfi 8232 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
Theorem | domunfican 8233 | A finite set union cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.) |
Theorem | infcntss 8234* | Every infinite set has a denumerable subset. Similar to Exercise 8 of [TakeutiZaring] p. 91. (However, we need neither AC nor the Axiom of Infinity because of the way we express "infinite" in the antecedent.) (Contributed by NM, 23-Oct-2004.) |
Theorem | prfi 8235 | An unordered pair is finite. (Contributed by NM, 22-Aug-2008.) |
Theorem | tpfi 8236 | An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.) |
Theorem | fiint 8237* | Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of is in ." This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.) |
Theorem | fnfi 8238 | A version of fnex 6481 for finite sets that does not require Replacement. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
Theorem | fodomfi 8239 | An onto function implies dominance of domain over range, for finite sets. Unlike fodom 9344 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) |
Theorem | fodomfib 8240* | Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 9348 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) |
Theorem | fofinf1o 8241 | Any surjection from one finite set to another of equal size must be a bijection. (Contributed by Mario Carneiro, 19-Aug-2014.) |
Theorem | rneqdmfinf1o 8242 | Any function from a finite set onto the same set must be a bijection. (Contributed by AV, 5-Jul-2021.) |
Theorem | fidomdm 8243 | Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
Theorem | dmfi 8244 | The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013.) |
Theorem | fundmfibi 8245 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
Theorem | resfnfinfin 8246 | The restriction of a function by a finite set is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.) |
Theorem | residfi 8247 | A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.) |
Theorem | cnvfi 8248 | If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) |
Theorem | rnfi 8249 | The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014.) |
Theorem | f1dmvrnfibi 8250 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 8251. (Contributed by AV, 10-Jan-2020.) |
Theorem | f1vrnfibi 8251 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 8250. (Contributed by AV, 10-Jan-2020.) |
Theorem | fofi 8252 | If a function has a finite domain, its range is finite. Theorem 37 of [Suppes] p. 104. (Contributed by NM, 25-Mar-2007.) |
Theorem | f1fi 8253 | If a 1-to-1 function has a finite codomain its domain is finite. (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 24-Jun-2015.) |
Theorem | iunfi 8254* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 8255. Note that depends on , i.e. can be thought of as . (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
Theorem | unifi 8255 | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. (Contributed by NM, 22-Aug-2008.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | unifi2 8256* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 8255 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 8223). (Contributed by NM, 11-Mar-2006.) |
Theorem | infssuni 8257* | If an infinite set is included in the underlying set of a finite cover , then there exists a set of the cover that contains an infinite number of element of . (Contributed by FL, 2-Aug-2009.) |
Theorem | unirnffid 8258 | The union of the range of a function from a finite set into the class of finite sets is finite. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Theorem | imafi 8259 | Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | pwfilem 8260* | Lemma for pwfi 8261. (Contributed by NM, 26-Mar-2007.) |
Theorem | pwfi 8261 | The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105. (Contributed by NM, 26-Mar-2007.) |
Theorem | mapfi 8262 | Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.) |
Theorem | ixpfi 8263* | A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.) |
Theorem | ixpfi2 8264* | A Cartesian product of finite sets such that all but finitely many are singletons is finite. (Note that and are both possibly dependent on .) (Contributed by Mario Carneiro, 25-Jan-2015.) |
Theorem | mptfi 8265* | A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015.) |
Theorem | abrexfi 8266* | An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014.) |
Theorem | cnvimamptfin 8267* | A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi 8283, the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018.) |
Theorem | elfpw 8268 | Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Theorem | unifpw 8269 | A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
Theorem | f1opwfi 8270* | A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015.) |
Theorem | fissuni 8271* | A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
Theorem | fipreima 8272* | Given a finite subset of the range of a function, there exists a finite subset of the domain whose image is . (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
Theorem | finsschain 8273* | A finite subset of the union of a superset chain is a subset of some element of the chain. A useful preliminary result for alexsub 21849 and others. (Contributed by Jeff Hankins, 25-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 18-May-2015.) |
[] | ||
Theorem | indexfi 8274* | If for every element of a finite indexing set there exists a corresponding element of another set , then there exists a finite subset of consisting only of those elements which are indexed by . Proven without the Axiom of Choice, unlike indexdom 33529. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
Syntax | cfsupp 8275 | Extend class definition to include the predicate to be a finitely supported function. |
finSupp | ||
Definition | df-fsupp 8276* | Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
finSupp supp | ||
Theorem | relfsupp 8277 | The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019.) |
finSupp | ||
Theorem | relprcnfsupp 8278 | A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.) |
finSupp | ||
Theorem | isfsupp 8279 | The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
finSupp supp | ||
Theorem | funisfsupp 8280 | The property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
finSupp supp | ||
Theorem | fsuppimp 8281 | Implications of a class being a finitely supported function (in relation to a given zero). (Contributed by AV, 26-May-2019.) |
finSupp supp | ||
Theorem | fsuppimpd 8282 | A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.) |
finSupp supp | ||
Theorem | fisuppfi 8283 | A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | fdmfisuppfi 8284 | The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019.) |
supp | ||
Theorem | fdmfifsupp 8285 | A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.) |
finSupp | ||
Theorem | fsuppmptdm 8286* | A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019.) |
finSupp | ||
Theorem | fndmfisuppfi 8287 | The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019.) |
supp | ||
Theorem | fndmfifsupp 8288 | A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.) |
finSupp | ||
Theorem | suppeqfsuppbi 8289 | If two functions have the same support, one function is finitely supported iff the other one is finitely supported. (Contributed by AV, 30-Jun-2019.) |
supp supp finSupp finSupp | ||
Theorem | suppssfifsupp 8290 | If the support of a function is a subset of a finite set, the function is finitely supported. (Contributed by AV, 15-Jul-2019.) |
supp finSupp | ||
Theorem | fsuppsssupp 8291 | If the support of a function is a subset of the support of a finitely supported function, the function is finitely supported. (Contributed by AV, 2-Jul-2019.) (Proof shortened by AV, 15-Jul-2019.) |
finSupp supp supp finSupp | ||
Theorem | fsuppxpfi 8292 | The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.) |
finSupp finSupp supp supp | ||
Theorem | fczfsuppd 8293 | A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.) |
finSupp | ||
Theorem | fsuppun 8294 | The union of two finitely supported functions is finitely supported (but not necessarily a function!). (Contributed by AV, 3-Jun-2019.) |
finSupp finSupp supp | ||
Theorem | fsuppunfi 8295 | The union of the support of two finitely supported functions is finite. (Contributed by AV, 1-Jul-2019.) |
finSupp finSupp supp supp | ||
Theorem | fsuppunbi 8296 | If the union of two classes/functions is a function, this union is finitely supported iff the two functions are finitely supported. (Contributed by AV, 18-Jun-2019.) |
finSupp finSupp finSupp | ||
Theorem | 0fsupp 8297 | The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.) |
finSupp | ||
Theorem | snopfsupp 8298 | A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.) |
finSupp | ||
Theorem | funsnfsupp 8299 | Finite support for a function extended by a singleton. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by AV, 19-Jul-2019.) |
finSupp finSupp | ||
Theorem | fsuppres 8300 | The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.) |
finSupp finSupp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |