![]() |
Metamath
Proof Explorer Theorem List (p. 94 of 479) | < 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isfinite2 9301 | 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.) |
β’ (π΄ βΊ Ο β π΄ β Fin) | ||
Theorem | nnsdomg 9302 | Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. In order to avoid the Axiom of Infinity, we include it as part of the antecedent. See nnsdom 9649 for the version without this sethood requirement. (Contributed by NM, 15-Jun-1998.) Avoid ax-pow 5364. (Revised by BTernaryTau, 7-Jan-2025.) |
β’ ((Ο β V β§ π΄ β Ο) β π΄ βΊ Ο) | ||
Theorem | nnsdomgOLD 9303 | Obsolete version of nnsdomg 9302 as of 7-Jan-2025. (Contributed by NM, 15-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((Ο β V β§ π΄ β Ο) β π΄ βΊ Ο) | ||
Theorem | isfiniteg 9304 | 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.) |
β’ (Ο β V β (π΄ β Fin β π΄ βΊ Ο)) | ||
Theorem | infsdomnn 9305 | An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5364. (Revised by BTernaryTau, 7-Jan-2025.) |
β’ ((Ο βΌ π΄ β§ π΅ β Ο) β π΅ βΊ π΄) | ||
Theorem | infsdomnnOLD 9306 | Obsolete version of infsdomnn 9305 as of 7-Jan-2025. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((Ο βΌ π΄ β§ π΅ β Ο) β π΅ βΊ π΄) | ||
Theorem | infn0 9307 | An infinite set is not empty. For a shorter proof using ax-un 7725, see infn0ALT 9308. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7725. (Revised by BTernaryTau, 8-Jan-2025.) |
β’ (Ο βΌ π΄ β π΄ β β ) | ||
Theorem | infn0ALT 9308 | Shorter proof of infn0 9307 using ax-un 7725. (Contributed by NM, 23-Oct-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Ο βΌ π΄ β π΄ β β ) | ||
Theorem | fin2inf 9309 | 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.) |
β’ (π΄ βΊ Ο β Ο β V) | ||
Theorem | unfilem1 9310* | 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.) |
β’ π΄ β Ο & β’ π΅ β Ο & β’ πΉ = (π₯ β π΅ β¦ (π΄ +o π₯)) β β’ ran πΉ = ((π΄ +o π΅) β π΄) | ||
Theorem | unfilem2 9311* | 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.) |
β’ π΄ β Ο & β’ π΅ β Ο & β’ πΉ = (π₯ β π΅ β¦ (π΄ +o π₯)) β β’ πΉ:π΅β1-1-ontoβ((π΄ +o π΅) β π΄) | ||
Theorem | unfilem3 9312 | 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.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β π΅ β ((π΄ +o π΅) β π΄)) | ||
Theorem | unfiOLD 9313 | Obsolete version of unfi 9172 as of 7-Aug-2024. (Contributed by NM, 16-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) β Fin) | ||
Theorem | unfir 9314 | If a union is finite, the operands are finite. Converse of unfi 9172. (Contributed by FL, 3-Aug-2009.) |
β’ ((π΄ βͺ π΅) β Fin β (π΄ β Fin β§ π΅ β Fin)) | ||
Theorem | unfi2 9315 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 9172 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9309). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
β’ ((π΄ βΊ Ο β§ π΅ βΊ Ο) β (π΄ βͺ π΅) βΊ Ο) | ||
Theorem | difinf 9316 | An infinite set π΄ minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.) |
β’ ((Β¬ π΄ β Fin β§ π΅ β Fin) β Β¬ (π΄ β π΅) β Fin) | ||
Theorem | xpfi 9317 | The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5364. (Revised by BTernaryTau, 10-Jan-2025.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ Γ π΅) β Fin) | ||
Theorem | xpfiOLD 9318 | Obsolete version of xpfi 9317 as of 10-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ Γ π΅) β Fin) | ||
Theorem | 3xpfi 9319 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
β’ (π β Fin β ((π Γ π) Γ π) β Fin) | ||
Theorem | domunfican 9320 | A finite set union cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.) |
β’ (((π΄ β Fin β§ π΅ β π΄) β§ ((π΄ β© π) = β β§ (π΅ β© π) = β )) β ((π΄ βͺ π) βΌ (π΅ βͺ π) β π βΌ π)) | ||
Theorem | infcntss 9321* | 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.) |
β’ π΄ β V β β’ (Ο βΌ π΄ β βπ₯(π₯ β π΄ β§ π₯ β Ο)) | ||
Theorem | prfi 9322 | An unordered pair is finite. (Contributed by NM, 22-Aug-2008.) |
β’ {π΄, π΅} β Fin | ||
Theorem | tpfi 9323 | An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.) |
β’ {π΄, π΅, πΆ} β Fin | ||
Theorem | fiint 9324* | 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.) |
β’ (βπ₯ β π΄ βπ¦ β π΄ (π₯ β© π¦) β π΄ β βπ₯((π₯ β π΄ β§ π₯ β β β§ π₯ β Fin) β β© π₯ β π΄)) | ||
Theorem | fodomfi 9325 | An onto function implies dominance of domain over range, for finite sets. Unlike fodom 10518 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.) |
β’ ((π΄ β Fin β§ πΉ:π΄βontoβπ΅) β π΅ βΌ π΄) | ||
Theorem | fodomfib 9326* | Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 10521 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) |
β’ (π΄ β Fin β ((π΄ β β β§ βπ π:π΄βontoβπ΅) β (β βΊ π΅ β§ π΅ βΌ π΄))) | ||
Theorem | fofinf1o 9327 | Any surjection from one finite set to another of equal size must be a bijection. (Contributed by Mario Carneiro, 19-Aug-2014.) |
β’ ((πΉ:π΄βontoβπ΅ β§ π΄ β π΅ β§ π΅ β Fin) β πΉ:π΄β1-1-ontoβπ΅) | ||
Theorem | rneqdmfinf1o 9328 | Any function from a finite set onto the same set must be a bijection. (Contributed by AV, 5-Jul-2021.) |
β’ ((π΄ β Fin β§ πΉ Fn π΄ β§ ran πΉ = π΄) β πΉ:π΄β1-1-ontoβπ΄) | ||
Theorem | fidomdm 9329 | Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ (πΉ β Fin β dom πΉ βΌ πΉ) | ||
Theorem | dmfi 9330 | The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013.) |
β’ (π΄ β Fin β dom π΄ β Fin) | ||
Theorem | fundmfibi 9331 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
β’ (Fun πΉ β (πΉ β Fin β dom πΉ β Fin)) | ||
Theorem | resfnfinfin 9332 | The restriction of a function to a finite set is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.) |
β’ ((πΉ Fn π΄ β§ π΅ β Fin) β (πΉ βΎ π΅) β Fin) | ||
Theorem | residfi 9333 | A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.) |
β’ (( I βΎ π΄) β Fin β π΄ β Fin) | ||
Theorem | cnvfiALT 9334 | Shorter proof of cnvfi 9180 using ax-pow 5364. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β Fin β β‘π΄ β Fin) | ||
Theorem | rnfi 9335 | The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014.) |
β’ (π΄ β Fin β ran π΄ β Fin) | ||
Theorem | f1dmvrnfibi 9336 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 9337. (Contributed by AV, 10-Jan-2020.) |
β’ ((π΄ β π β§ πΉ:π΄β1-1βπ΅) β (πΉ β Fin β ran πΉ β Fin)) | ||
Theorem | f1vrnfibi 9337 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 9336. (Contributed by AV, 10-Jan-2020.) |
β’ ((πΉ β π β§ πΉ:π΄β1-1βπ΅) β (πΉ β Fin β ran πΉ β Fin)) | ||
Theorem | fofi 9338 | If an onto function has a finite domain, its codomain/range is finite. Theorem 37 of [Suppes] p. 104. (Contributed by NM, 25-Mar-2007.) |
β’ ((π΄ β Fin β§ πΉ:π΄βontoβπ΅) β π΅ β Fin) | ||
Theorem | f1fi 9339 | 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.) |
β’ ((π΅ β Fin β§ πΉ:π΄β1-1βπ΅) β π΄ β Fin) | ||
Theorem | iunfi 9340* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 9341. 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.) |
β’ ((π΄ β Fin β§ βπ₯ β π΄ π΅ β Fin) β βͺ π₯ β π΄ π΅ β Fin) | ||
Theorem | unifi 9341 | 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.) |
β’ ((π΄ β Fin β§ π΄ β Fin) β βͺ π΄ β Fin) | ||
Theorem | unifi2 9342* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 9341 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9309). (Contributed by NM, 11-Mar-2006.) |
β’ ((π΄ βΊ Ο β§ βπ₯ β π΄ π₯ βΊ Ο) β βͺ π΄ βΊ Ο) | ||
Theorem | infssuni 9343* | 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.) |
β’ ((Β¬ π΄ β Fin β§ π΅ β Fin β§ π΄ β βͺ π΅) β βπ₯ β π΅ Β¬ (π΄ β© π₯) β Fin) | ||
Theorem | unirnffid 9344 | 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.) |
β’ (π β πΉ:πβΆFin) & β’ (π β π β Fin) β β’ (π β βͺ ran πΉ β Fin) | ||
Theorem | imafiALT 9345 | Shorter proof of imafi 9175 using ax-pow 5364. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((Fun πΉ β§ π β Fin) β (πΉ β π) β Fin) | ||
Theorem | pwfilemOLD 9346* | Obsolete version of pwfilem 9177 as of 7-Sep-2024. (Contributed by NM, 26-Mar-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΉ = (π β π« π β¦ (π βͺ {π₯})) β β’ (π« π β Fin β π« (π βͺ {π₯}) β Fin) | ||
Theorem | pwfiOLD 9347 | Obsolete version of pwfi 9178 as of 7-Sep-2024. (Contributed by NM, 26-Mar-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β Fin β π« π΄ β Fin) | ||
Theorem | mapfi 9348 | Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βm π΅) β Fin) | ||
Theorem | ixpfi 9349* | A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.) |
β’ ((π΄ β Fin β§ βπ₯ β π΄ π΅ β Fin) β Xπ₯ β π΄ π΅ β Fin) | ||
Theorem | ixpfi2 9350* | 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.) |
β’ (π β πΆ β Fin) & β’ ((π β§ π₯ β π΄) β π΅ β Fin) & β’ ((π β§ π₯ β (π΄ β πΆ)) β π΅ β {π·}) β β’ (π β Xπ₯ β π΄ π΅ β Fin) | ||
Theorem | mptfi 9351* | A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015.) |
β’ (π΄ β Fin β (π₯ β π΄ β¦ π΅) β Fin) | ||
Theorem | abrexfi 9352* | An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014.) |
β’ (π΄ β Fin β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β Fin) | ||
Theorem | cnvimamptfin 9353* | A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi 9370, the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018.) |
β’ (π β π β Fin) β β’ (π β (β‘(π β π β¦ π) β π) β Fin) | ||
Theorem | elfpw 9354 | Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π΄ β (π« π΅ β© Fin) β (π΄ β π΅ β§ π΄ β Fin)) | ||
Theorem | unifpw 9355 | A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ βͺ (π« π΄ β© Fin) = π΄ | ||
Theorem | f1opwfi 9356* | A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015.) |
β’ (πΉ:π΄β1-1-ontoβπ΅ β (π β (π« π΄ β© Fin) β¦ (πΉ β π)):(π« π΄ β© Fin)β1-1-ontoβ(π« π΅ β© Fin)) | ||
Theorem | fissuni 9357* | A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ ((π΄ β βͺ π΅ β§ π΄ β Fin) β βπ β (π« π΅ β© Fin)π΄ β βͺ π) | ||
Theorem | fipreima 9358* | 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.) |
β’ ((πΉ Fn π΅ β§ π΄ β ran πΉ β§ π΄ β Fin) β βπ β (π« π΅ β© Fin)(πΉ β π) = π΄) | ||
Theorem | finsschain 9359* | 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 23549 and others. (Contributed by Jeff Hankins, 25-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 18-May-2015.) |
β’ (((π΄ β β β§ [β] Or π΄) β§ (π΅ β Fin β§ π΅ β βͺ π΄)) β βπ§ β π΄ π΅ β π§) | ||
Theorem | indexfi 9360* | 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 36602. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π΄ β Fin β§ π΅ β π β§ βπ₯ β π΄ βπ¦ β π΅ π) β βπ β Fin (π β π΅ β§ βπ₯ β π΄ βπ¦ β π π β§ βπ¦ β π βπ₯ β π΄ π)) | ||
Syntax | cfsupp 9361 | Extend class definition to include the predicate to be a finitely supported function. |
class finSupp | ||
Definition | df-fsupp 9362* | Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
β’ finSupp = {β¨π, π§β© β£ (Fun π β§ (π supp π§) β Fin)} | ||
Theorem | relfsupp 9363 | The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019.) |
β’ Rel finSupp | ||
Theorem | relprcnfsupp 9364 | A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.) |
β’ (Β¬ π΄ β V β Β¬ π΄ finSupp π) | ||
Theorem | isfsupp 9365 | The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
β’ ((π β π β§ π β π) β (π finSupp π β (Fun π β§ (π supp π) β Fin))) | ||
Theorem | isfsuppd 9366 | Deduction form of isfsupp 9365. (Contributed by SN, 29-Jul-2024.) |
β’ (π β π β π) & β’ (π β π β π) & β’ (π β Fun π ) & β’ (π β (π supp π) β Fin) β β’ (π β π finSupp π) | ||
Theorem | funisfsupp 9367 | The property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
β’ ((Fun π β§ π β π β§ π β π) β (π finSupp π β (π supp π) β Fin)) | ||
Theorem | fsuppimp 9368 | Implications of a class being a finitely supported function (in relation to a given zero). (Contributed by AV, 26-May-2019.) |
β’ (π finSupp π β (Fun π β§ (π supp π) β Fin)) | ||
Theorem | fsuppimpd 9369 | A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.) |
β’ (π β πΉ finSupp π) β β’ (π β (πΉ supp π) β Fin) | ||
Theorem | fisuppfi 9370 | A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (π β π΄ β Fin) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (β‘πΉ β πΆ) β Fin) | ||
Theorem | fidmfisupp 9371 | A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β πΉ:π·βΆπ ) & β’ (π β π· β Fin) & β’ (π β π β π) β β’ (π β πΉ finSupp π) | ||
Theorem | fdmfisuppfi 9372 | The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019.) |
β’ (π β πΉ:π·βΆπ ) & β’ (π β π· β Fin) & β’ (π β π β π) β β’ (π β (πΉ supp π) β Fin) | ||
Theorem | fdmfifsupp 9373 | A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.) |
β’ (π β πΉ:π·βΆπ ) & β’ (π β π· β Fin) & β’ (π β π β π) β β’ (π β πΉ finSupp π) | ||
Theorem | fsuppmptdm 9374* | A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π β π) & β’ (π β π β π) β β’ (π β πΉ finSupp π) | ||
Theorem | fndmfisuppfi 9375 | The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019.) |
β’ (π β πΉ Fn π·) & β’ (π β π· β Fin) & β’ (π β π β π) β β’ (π β (πΉ supp π) β Fin) | ||
Theorem | fndmfifsupp 9376 | A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.) |
β’ (π β πΉ Fn π·) & β’ (π β π· β Fin) & β’ (π β π β π) β β’ (π β πΉ finSupp π) | ||
Theorem | suppeqfsuppbi 9377 | 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.) |
β’ (((πΉ β π β§ Fun πΉ) β§ (πΊ β π β§ Fun πΊ)) β ((πΉ supp π) = (πΊ supp π) β (πΉ finSupp π β πΊ finSupp π))) | ||
Theorem | suppssfifsupp 9378 | If the support of a function is a subset of a finite set, the function is finitely supported. (Contributed by AV, 15-Jul-2019.) |
β’ (((πΊ β π β§ Fun πΊ β§ π β π) β§ (πΉ β Fin β§ (πΊ supp π) β πΉ)) β πΊ finSupp π) | ||
Theorem | fsuppsssupp 9379 | 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.) |
β’ (((πΊ β π β§ Fun πΊ) β§ (πΉ finSupp π β§ (πΊ supp π) β (πΉ supp π))) β πΊ finSupp π) | ||
Theorem | fsuppxpfi 9380 | The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.) |
β’ ((πΉ finSupp π β§ πΊ finSupp π) β ((πΉ supp π) Γ (πΊ supp π)) β Fin) | ||
Theorem | fczfsuppd 9381 | A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.) |
β’ (π β π΅ β π) & β’ (π β π β π) β β’ (π β (π΅ Γ {π}) finSupp π) | ||
Theorem | fsuppun 9382 | The union of two finitely supported functions is finitely supported (but not necessarily a function!). (Contributed by AV, 3-Jun-2019.) |
β’ (π β πΉ finSupp π) & β’ (π β πΊ finSupp π) β β’ (π β ((πΉ βͺ πΊ) supp π) β Fin) | ||
Theorem | fsuppunfi 9383 | The union of the support of two finitely supported functions is finite. (Contributed by AV, 1-Jul-2019.) |
β’ (π β πΉ finSupp π) & β’ (π β πΊ finSupp π) β β’ (π β ((πΉ supp π) βͺ (πΊ supp π)) β Fin) | ||
Theorem | fsuppunbi 9384 | 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.) |
β’ (π β Fun (πΉ βͺ πΊ)) β β’ (π β ((πΉ βͺ πΊ) finSupp π β (πΉ finSupp π β§ πΊ finSupp π))) | ||
Theorem | 0fsupp 9385 | The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.) |
β’ (π β π β β finSupp π) | ||
Theorem | snopfsupp 9386 | A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.) |
β’ ((π β π β§ π β π β§ π β π) β {β¨π, πβ©} finSupp π) | ||
Theorem | funsnfsupp 9387 | Finite support for a function extended by a singleton. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by AV, 19-Jul-2019.) |
β’ (((π β π β§ π β π) β§ (Fun πΉ β§ π β dom πΉ)) β ((πΉ βͺ {β¨π, πβ©}) finSupp π β πΉ finSupp π)) | ||
Theorem | fsuppres 9388 | The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.) |
β’ (π β πΉ finSupp π) & β’ (π β π β π) β β’ (π β (πΉ βΎ π) finSupp π) | ||
Theorem | fmptssfisupp 9389* | The restriction of a mapping function has finite support if that function has finite support. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ (π β (π₯ β π΄ β¦ π΅) finSupp π) & β’ (π β πΆ β π΄) & β’ (π β π β π) β β’ (π β (π₯ β πΆ β¦ π΅) finSupp π) | ||
Theorem | ressuppfi 9390 | If the support of the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finite, the support of the function itself is finite. (Contributed by AV, 22-Apr-2019.) |
β’ (π β (dom πΉ β π΅) β Fin) & β’ (π β πΉ β π) & β’ (π β πΊ = (πΉ βΎ π΅)) & β’ (π β (πΊ supp π) β Fin) & β’ (π β π β π) β β’ (π β (πΉ supp π) β Fin) | ||
Theorem | resfsupp 9391 | If the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finitely supported, the function itself is finitely supported. (Contributed by AV, 27-May-2019.) |
β’ (π β (dom πΉ β π΅) β Fin) & β’ (π β πΉ β π) & β’ (π β Fun πΉ) & β’ (π β πΊ = (πΉ βΎ π΅)) & β’ (π β πΊ finSupp π) & β’ (π β π β π) β β’ (π β πΉ finSupp π) | ||
Theorem | resfifsupp 9392 | The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.) |
β’ (π β Fun πΉ) & β’ (π β π β Fin) & β’ (π β π β π) β β’ (π β (πΉ βΎ π) finSupp π) | ||
Theorem | ffsuppbi 9393 | Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019.) |
β’ ((πΌ β π β§ π β π) β (πΉ:πΌβΆπ β (πΉ finSupp π β (β‘πΉ β (π β {π})) β Fin))) | ||
Theorem | fsuppmptif 9394* | A function mapping an argument to either a value of a finitely supported function or zero is finitely supported. (Contributed by AV, 6-Jun-2019.) |
β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β πΉ finSupp π) β β’ (π β (π β π΄ β¦ if(π β π·, (πΉβπ), π)) finSupp π) | ||
Theorem | sniffsupp 9395* | A function mapping all but one arguments to zero is finitely supported. (Contributed by AV, 8-Jul-2019.) |
β’ (π β πΌ β π) & β’ (π β 0 β π) & β’ πΉ = (π₯ β πΌ β¦ if(π₯ = π, π΄, 0 )) β β’ (π β πΉ finSupp 0 ) | ||
Theorem | fsuppcolem 9396 | Lemma for fsuppco 9397. Formula building theorem for finite supports: rearranging the index set. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
β’ (π β (β‘πΉ β (V β {π})) β Fin) & β’ (π β πΊ:πβ1-1βπ) β β’ (π β (β‘(πΉ β πΊ) β (V β {π})) β Fin) | ||
Theorem | fsuppco 9397 | The composition of a 1-1 function with a finitely supported function is finitely supported. (Contributed by AV, 28-May-2019.) |
β’ (π β πΉ finSupp π) & β’ (π β πΊ:πβ1-1βπ) & β’ (π β π β π) & β’ (π β πΉ β π) β β’ (π β (πΉ β πΊ) finSupp π) | ||
Theorem | fsuppco2 9398 | The composition of a function which maps the zero to zero with a finitely supported function is finitely supported. This is not only a special case of fsuppcor 9399 because it does not require that the "zero" is an element of the range of the finitely supported function. (Contributed by AV, 6-Jun-2019.) |
β’ (π β π β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΊ:π΅βΆπ΅) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ finSupp π) & β’ (π β (πΊβπ) = π) β β’ (π β (πΊ β πΉ) finSupp π) | ||
Theorem | fsuppcor 9399 | The composition of a function which maps the zero of the range of a finitely supported function to the zero of its range with this finitely supported function is finitely supported. (Contributed by AV, 6-Jun-2019.) |
β’ (π β 0 β π) & β’ (π β π β π΅) & β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπ·) & β’ (π β πΆ β π΅) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ finSupp π) & β’ (π β (πΊβπ) = 0 ) β β’ (π β (πΊ β πΉ) finSupp 0 ) | ||
Theorem | mapfienlem1 9400* | Lemma 1 for mapfien 9403. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} & β’ π = {π₯ β (π· βm πΆ) β£ π₯ finSupp π} & β’ π = (πΊβπ) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ (π β πΊ:π΅β1-1-ontoβπ·) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π β π΅) β β’ ((π β§ π β π) β (πΊ β (π β πΉ)) finSupp π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |