Home | Metamath
Proof Explorer Theorem List (p. 91 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 | sdomel 9001 | For ordinals, strict dominance implies membership. (Contributed by Mario Carneiro, 13-Jan-2013.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ βΊ π΅ β π΄ β π΅)) | ||
Theorem | sdomdif 9002 | The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013.) |
β’ (π΄ βΊ π΅ β (π΅ β π΄) β β ) | ||
Theorem | onsdominel 9003 | An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
β’ ((π΄ β On β§ π΅ β On β§ (π΄ β© πΆ) βΊ (π΅ β© πΆ)) β π΄ β π΅) | ||
Theorem | domunsn 9004 | Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π΄ βΊ π΅ β (π΄ βͺ {πΆ}) βΌ π΅) | ||
Theorem | fodomr 9005* | There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.) |
β’ ((β βΊ π΅ β§ π΅ βΌ π΄) β βπ π:π΄βontoβπ΅) | ||
Theorem | pwdom 9006 | Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ (π΄ βΌ π΅ β π« π΄ βΌ π« π΅) | ||
Theorem | canth2 9007 | Cantor's Theorem. No set is equinumerous to its power set. Specifically, any set has a cardinality (size) strictly less than the cardinality of its power set. For example, the cardinality of real numbers is the same as the cardinality of the power set of integers, so real numbers cannot be put into a one-to-one correspondence with integers. Theorem 23 of [Suppes] p. 97. For the function version, see canth 7302. This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994.) |
β’ π΄ β V β β’ π΄ βΊ π« π΄ | ||
Theorem | canth2g 9008 | Cantor's theorem with the sethood requirement expressed as an antecedent. Theorem 23 of [Suppes] p. 97. (Contributed by NM, 7-Nov-2003.) |
β’ (π΄ β π β π΄ βΊ π« π΄) | ||
Theorem | 2pwuninel 9009 | The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by NM, 27-Jun-2008.) |
β’ Β¬ π« π« βͺ π΄ β π΄ | ||
Theorem | 2pwne 9010 | No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.) |
β’ (π΄ β π β π« π« π΄ β π΄) | ||
Theorem | disjen 9011 | A stronger form of pwuninel 8173. We can use pwuninel 8173, 2pwuninel 9009 to create one or two sets disjoint from a given set π΄, but here we show that in fact such constructions exist for arbitrarily large disjoint extensions, which is to say that for any set π΅ we can construct a set π₯ that is equinumerous to it and disjoint from π΄. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ ((π΄ β π β§ π΅ β π) β ((π΄ β© (π΅ Γ {π« βͺ ran π΄})) = β β§ (π΅ Γ {π« βͺ ran π΄}) β π΅)) | ||
Theorem | disjenex 9012* | Existence version of disjen 9011. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ ((π΄ β π β§ π΅ β π) β βπ₯((π΄ β© π₯) = β β§ π₯ β π΅)) | ||
Theorem | domss2 9013 | A corollary of disjenex 9012. If πΉ is an injection from π΄ to π΅ then πΊ is a right inverse of πΉ from π΅ to a superset of π΄. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
β’ πΊ = β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (πΊ:π΅β1-1-ontoβran πΊ β§ π΄ β ran πΊ β§ (πΊ β πΉ) = ( I βΎ π΄))) | ||
Theorem | domssex2 9014* | A corollary of disjenex 9012. If πΉ is an injection from π΄ to π΅ then there is a right inverse π of πΉ from π΅ to a superset of π΄. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β βπ(π:π΅β1-1βV β§ (π β πΉ) = ( I βΎ π΄))) | ||
Theorem | domssex 9015* | Weakening of domssex2 9014 to forget the functions in favor of dominance and equinumerosity. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
β’ (π΄ βΌ π΅ β βπ₯(π΄ β π₯ β§ π΅ β π₯)) | ||
Theorem | xpf1o 9016* | Construct a bijection on a Cartesian product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015.) |
β’ (π β (π₯ β π΄ β¦ π):π΄β1-1-ontoβπ΅) & β’ (π β (π¦ β πΆ β¦ π):πΆβ1-1-ontoβπ·) β β’ (π β (π₯ β π΄, π¦ β πΆ β¦ β¨π, πβ©):(π΄ Γ πΆ)β1-1-ontoβ(π΅ Γ π·)) | ||
Theorem | xpen 9017 | Equinumerosity law for Cartesian product. Proposition 4.22(b) of [Mendelson] p. 254. (Contributed by NM, 24-Jul-2004.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
β’ ((π΄ β π΅ β§ πΆ β π·) β (π΄ Γ πΆ) β (π΅ Γ π·)) | ||
Theorem | mapen 9018 | Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of [Enderton] p. 139. (Contributed by NM, 16-Dec-2003.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
β’ ((π΄ β π΅ β§ πΆ β π·) β (π΄ βm πΆ) β (π΅ βm π·)) | ||
Theorem | mapdom1 9019 | Order-preserving property of set exponentiation. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.) |
β’ (π΄ βΌ π΅ β (π΄ βm πΆ) βΌ (π΅ βm πΆ)) | ||
Theorem | mapxpen 9020 | Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96. (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2015.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β ((π΄ βm π΅) βm πΆ) β (π΄ βm (π΅ Γ πΆ))) | ||
Theorem | xpmapenlem 9021* | Lemma for xpmapen 9022. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V & β’ π· = (π§ β πΆ β¦ (1st β(π₯βπ§))) & β’ π = (π§ β πΆ β¦ (2nd β(π₯βπ§))) & β’ π = (π§ β πΆ β¦ β¨((1st βπ¦)βπ§), ((2nd βπ¦)βπ§)β©) β β’ ((π΄ Γ π΅) βm πΆ) β ((π΄ βm πΆ) Γ (π΅ βm πΆ)) | ||
Theorem | xpmapen 9022 | Equinumerosity law for set exponentiation of a Cartesian product. Exercise 4.47 of [Mendelson] p. 255. (Contributed by NM, 23-Feb-2004.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ ((π΄ Γ π΅) βm πΆ) β ((π΄ βm πΆ) Γ (π΅ βm πΆ)) | ||
Theorem | mapunen 9023 | Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β© π΅) = β ) β (πΆ βm (π΄ βͺ π΅)) β ((πΆ βm π΄) Γ (πΆ βm π΅))) | ||
Theorem | map2xp 9024 | A cardinal power with exponent 2 is equivalent to a Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by AV, 17-Jul-2022.) |
β’ (π΄ β π β (π΄ βm 2o) β (π΄ Γ π΄)) | ||
Theorem | mapdom2 9025 | Order-preserving property of set exponentiation. Theorem 6L(d) of [Enderton] p. 149. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ ((π΄ βΌ π΅ β§ Β¬ (π΄ = β β§ πΆ = β )) β (πΆ βm π΄) βΌ (πΆ βm π΅)) | ||
Theorem | mapdom3 9026 | Set exponentiation dominates the base. (Contributed by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 17-Jul-2022.) |
β’ ((π΄ β π β§ π΅ β π β§ π΅ β β ) β π΄ βΌ (π΄ βm π΅)) | ||
Theorem | pwen 9027 | If two sets are equinumerous, then their power sets are equinumerous. Proposition 10.15 of [TakeutiZaring] p. 87. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 9-Apr-2015.) |
β’ (π΄ β π΅ β π« π΄ β π« π΅) | ||
Theorem | ssenen 9028* | Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ (π΄ β π΅ β {π₯ β£ (π₯ β π΄ β§ π₯ β πΆ)} β {π₯ β£ (π₯ β π΅ β§ π₯ β πΆ)}) | ||
Theorem | limenpsi 9029 | A limit ordinal is equinumerous to a proper subset of itself. (Contributed by NM, 30-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ Lim π΄ β β’ (π΄ β π β π΄ β (π΄ β {β })) | ||
Theorem | limensuci 9030 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ Lim π΄ β β’ (π΄ β π β π΄ β suc π΄) | ||
Theorem | limensuc 9031 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ ((π΄ β π β§ Lim π΄) β π΄ β suc π΄) | ||
Theorem | infensuc 9032 | Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88. Proved without the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.) (Revised by Mario Carneiro, 13-Jan-2013.) |
β’ ((π΄ β On β§ Ο β π΄) β π΄ β suc π΄) | ||
Theorem | dif1enlem 9033 | Lemma for rexdif1en 9035 and dif1en 9037. (Contributed by BTernaryTau, 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to avoid ax-un 7662. (Revised by BTernaryTau, 5-Jan-2025.) |
β’ (((πΉ β π β§ π΄ β π β§ π β On) β§ πΉ:π΄β1-1-ontoβsuc π) β (π΄ β {(β‘πΉβπ)}) β π) | ||
Theorem | dif1enlemOLD 9034 | Obsolete version of dif1enlem 9033 as of 5-Jan-2025. (Contributed by BTernaryTau, 18-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((πΉ β π β§ π β Ο β§ πΉ:π΄β1-1-ontoβsuc π) β (π΄ β {(β‘πΉβπ)}) β π) | ||
Theorem | rexdif1en 9035* | If a set is equinumerous to a nonzero ordinal, then there exists an element in that set such that removing it leaves the set equinumerous to the predecessor of that ordinal. (Contributed by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals and avoid ax-un 7662. (Revised by BTernaryTau, 5-Jan-2025.) |
β’ ((π β On β§ π΄ β suc π) β βπ₯ β π΄ (π΄ β {π₯}) β π) | ||
Theorem | rexdif1enOLD 9036* | Obsolete version of rexdif1en 9035 as of 5-Jan-2025. (Contributed by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Ο β§ π΄ β suc π) β βπ₯ β π΄ (π΄ β {π₯}) β π) | ||
Theorem | dif1en 9037 | If a set π΄ is equinumerous to the successor of an ordinal π, then π΄ with an element removed is equinumerous to π. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5318. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.) |
β’ ((π β On β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | dif1ennn 9038 | If a set π΄ is equinumerous to the successor of a natural number π, then π΄ with an element removed is equinumerous to π. See also dif1ennnALT 9154. (Contributed by BTernaryTau, 6-Jan-2025.) |
β’ ((π β Ο β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | dif1enOLD 9039 | Obsolete version of dif1en 9037 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5318. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Ο β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | findcard 9040* | Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = (π¦ β {π§}) β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β Fin β (βπ§ β π¦ π β π)) β β’ (π΄ β Fin β π) | ||
Theorem | findcard2 9041* | Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.) Avoid ax-pow 5318. (Revised by BTernaryTau, 26-Aug-2024.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β Fin β (π β π)) β β’ (π΄ β Fin β π) | ||
Theorem | findcard2s 9042* | Variation of findcard2 9041 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β (π β π)) β β’ (π΄ β Fin β π) | ||
Theorem | findcard2d 9043* | Deduction version of findcard2 9041. (Contributed by SO, 16-Jul-2018.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π β π) & β’ ((π β§ (π¦ β π΄ β§ π§ β (π΄ β π¦))) β (π β π)) & β’ (π β π΄ β Fin) β β’ (π β π) | ||
Theorem | nnfi 9044 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5318. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ (π΄ β Ο β π΄ β Fin) | ||
Theorem | pssnn 9045* | A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of [Enderton] p. 137. (Contributed by NM, 22-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) Avoid ax-pow 5318. (Revised by BTernaryTau, 31-Jul-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β βπ₯ β π΄ π΅ β π₯) | ||
Theorem | ssnnfi 9046 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | ssnnfiOLD 9047 | Obsolete version of ssnnfi 9046 as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | 0fin 9048 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
β’ β β Fin | ||
Theorem | unfi 9049 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.) Avoid ax-pow 5318. (Revised by BTernaryTau, 7-Aug-2024.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) β Fin) | ||
Theorem | ssfi 9050 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5318, see ssfiALT 9051. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5318. (Revised by BTernaryTau, 12-Aug-2024.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | ssfiALT 9051 | Shorter proof of ssfi 9050 using ax-pow 5318. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | imafi 9052 | Images of finite sets are finite. For a shorter proof using ax-pow 5318, see imafiALT 9222. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5318. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ ((Fun πΉ β§ π β Fin) β (πΉ β π) β Fin) | ||
Theorem | pwfir 9053 | If the power set of a set is finite, then the set itself is finite. (Contributed by BTernaryTau, 7-Sep-2024.) |
β’ (π« π΅ β Fin β π΅ β Fin) | ||
Theorem | pwfilem 9054* | Lemma for pwfi 9055. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5318. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ πΉ = (π β π« π β¦ (π βͺ {π₯})) β β’ (π« π β Fin β π« (π βͺ {π₯}) β Fin) | ||
Theorem | pwfi 9055 | 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.) Avoid ax-pow 5318. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ (π΄ β Fin β π« π΄ β Fin) | ||
Theorem | diffi 9056 | If π΄ is finite, (π΄ β π΅) is finite. (Contributed by FL, 3-Aug-2009.) |
β’ (π΄ β Fin β (π΄ β π΅) β Fin) | ||
Theorem | cnvfi 9057 | If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) Avoid ax-pow 5318. (Revised by BTernaryTau, 9-Sep-2024.) |
β’ (π΄ β Fin β β‘π΄ β Fin) | ||
Theorem | fnfi 9058 | A version of fnex 7161 for finite sets that does not require Replacement or Power Sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
β’ ((πΉ Fn π΄ β§ π΄ β Fin) β πΉ β Fin) | ||
Theorem | f1oenfi 9059 | If the domain of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1oeng 8844). (Contributed by BTernaryTau, 8-Sep-2024.) |
β’ ((π΄ β Fin β§ πΉ:π΄β1-1-ontoβπ΅) β π΄ β π΅) | ||
Theorem | f1oenfirn 9060 | If the range of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. (Contributed by BTernaryTau, 9-Sep-2024.) |
β’ ((π΅ β Fin β§ πΉ:π΄β1-1-ontoβπ΅) β π΄ β π΅) | ||
Theorem | f1domfi 9061 | If the codomain of a one-to-one function is finite, then the function's domain is dominated by its codomain. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1domg 8845). (Contributed by BTernaryTau, 25-Sep-2024.) |
β’ ((π΅ β Fin β§ πΉ:π΄β1-1βπ΅) β π΄ βΌ π΅) | ||
Theorem | f1domfi2 9062 | If the domain of a one-to-one function is finite, then the function's domain is dominated by its codomain when the latter is a set. This theorem is proved without using the Axiom of Power Sets (unlike f1dom2g 8842). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π β§ πΉ:π΄β1-1βπ΅) β π΄ βΌ π΅) | ||
Theorem | enreffi 9063 | Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg 8857). (Contributed by BTernaryTau, 8-Sep-2024.) |
β’ (π΄ β Fin β π΄ β π΄) | ||
Theorem | ensymfib 9064 | Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb 8875). (Contributed by BTernaryTau, 9-Sep-2024.) |
β’ (π΄ β Fin β (π΄ β π΅ β π΅ β π΄)) | ||
Theorem | entrfil 9065 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8879). (Contributed by BTernaryTau, 10-Sep-2024.) |
β’ ((π΄ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | enfii 9066 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5318. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ ((π΅ β Fin β§ π΄ β π΅) β π΄ β Fin) | ||
Theorem | enfi 9067 | Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5318, see enfiALT 9068. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5318. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ (π΄ β π΅ β (π΄ β Fin β π΅ β Fin)) | ||
Theorem | enfiALT 9068 | Shorter proof of enfi 9067 using ax-pow 5318. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β π΅ β (π΄ β Fin β π΅ β Fin)) | ||
Theorem | domfi 9069 | A set dominated by a finite set is finite. (Contributed by NM, 23-Mar-2006.) (Revised by Mario Carneiro, 12-Mar-2015.) |
β’ ((π΄ β Fin β§ π΅ βΌ π΄) β π΅ β Fin) | ||
Theorem | entrfi 9070 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8879). (Contributed by BTernaryTau, 23-Sep-2024.) |
β’ ((π΅ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | entrfir 9071 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8879). (Contributed by BTernaryTau, 23-Sep-2024.) |
β’ ((πΆ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | domtrfil 9072 | Transitivity of dominance relation when π΄ is finite, proved without using the Axiom of Power Sets (unlike domtr 8880). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | domtrfi 9073 | Transitivity of dominance relation when π΅ is finite, proved without using the Axiom of Power Sets (unlike domtr 8880). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | domtrfir 9074 | Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 8880). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((πΆ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | f1imaenfi 9075 | If a function is one-to-one, then the image of a finite subset of its domain under it is equinumerous to the subset. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1imaeng 8887). (Contributed by BTernaryTau, 29-Sep-2024.) |
β’ ((πΉ:π΄β1-1βπ΅ β§ πΆ β π΄ β§ πΆ β Fin) β (πΉ β πΆ) β πΆ) | ||
Theorem | ssdomfi 9076 | A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8873). (Contributed by BTernaryTau, 12-Nov-2024.) |
β’ (π΅ β Fin β (π΄ β π΅ β π΄ βΌ π΅)) | ||
Theorem | ssdomfi2 9077 | A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8873). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π β§ π΄ β π΅) β π΄ βΌ π΅) | ||
Theorem | sbthfilem 9078* | Lemma for sbthfi 9079. (Contributed by BTernaryTau, 4-Nov-2024.) |
β’ π΄ β V & β’ π· = {π₯ β£ (π₯ β π΄ β§ (π β (π΅ β (π β π₯))) β (π΄ β π₯))} & β’ π» = ((π βΎ βͺ π·) βͺ (β‘π βΎ (π΄ β βͺ π·))) & β’ π΅ β V β β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ π΄) β π΄ β π΅) | ||
Theorem | sbthfi 9079 | Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 8970). (Contributed by BTernaryTau, 4-Nov-2024.) |
β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ π΄) β π΄ β π΅) | ||
Theorem | domnsymfi 9080 | If a set dominates a finite set, it cannot also be strictly dominated by the finite set. This theorem is proved without using the Axiom of Power Sets (unlike domnsym 8976). (Contributed by BTernaryTau, 22-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅) β Β¬ π΅ βΊ π΄) | ||
Theorem | sdomdomtrfi 9081 | Transitivity of strict dominance and dominance when π΄ is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 8987). (Contributed by BTernaryTau, 25-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΊ π΅ β§ π΅ βΌ πΆ) β π΄ βΊ πΆ) | ||
Theorem | domsdomtrfi 9082 | Transitivity of dominance and strict dominance when π΄ is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 8989). (Contributed by BTernaryTau, 25-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅ β§ π΅ βΊ πΆ) β π΄ βΊ πΆ) | ||
Theorem | sucdom2 9083 | Strict dominance of a set over another set implies dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5318. (Revised by BTernaryTau, 4-Dec-2024.) |
β’ (π΄ βΊ π΅ β suc π΄ βΌ π΅) | ||
Theorem | phplem1 9084 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998.) Avoid ax-pow 5318. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ ((π΄ β Ο β§ π΅ β suc π΄) β π΄ β (suc π΄ β {π΅})) | ||
Theorem | phplem2 9085 | Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) Avoid ax-pow 5318. (Revised by BTernaryTau, 4-Nov-2024.) |
β’ π΄ β V β β’ ((π΄ β Ο β§ π΅ β Ο) β (suc π΄ β suc π΅ β π΄ β π΅)) | ||
Theorem | nneneq 9086 | Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136. (Contributed by NM, 28-May-1998.) Avoid ax-pow 5318. (Revised by BTernaryTau, 11-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅ β π΄ = π΅)) | ||
Theorem | php 9087 | Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of phplem1 9084, phplem2 9085, nneneq 9086, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5318. (Revised by BTernaryTau, 18-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β Β¬ π΄ β π΅) | ||
Theorem | php2 9088 | Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5318. (Revised by BTernaryTau, 20-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ βΊ π΄) | ||
Theorem | php3 9089 | Corollary of Pigeonhole Principle. If π΄ is finite and π΅ is a proper subset of π΄, the π΅ is strictly less numerous than π΄. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5318. (Revised by BTernaryTau, 26-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ βΊ π΄) | ||
Theorem | php4 9090 | Corollary of the Pigeonhole Principle php 9087: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.) |
β’ (π΄ β Ο β π΄ βΊ suc π΄) | ||
Theorem | php5 9091 | Corollary of the Pigeonhole Principle php 9087: a natural number is not equinumerous to its successor. Corollary 10.21(1) of [TakeutiZaring] p. 90. (Contributed by NM, 26-Jul-2004.) |
β’ (π΄ β Ο β Β¬ π΄ β suc π΄) | ||
Theorem | phpeqd 9092 | Corollary of the Pigeonhole Principle using equality. Strengthening of php 9087 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow. (Revised by BTernaryTau, 28-Nov-2024.) |
β’ (π β π΄ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π΄ β π΅) β β’ (π β π΄ = π΅) | ||
Theorem | nndomog 9093 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9110 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9110. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5318. (Revised by BTernaryTau, 29-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β On) β (π΄ βΌ π΅ β π΄ β π΅)) | ||
Theorem | phplem1OLD 9094 | Obsolete lemma for php 9087. (Contributed by NM, 25-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β ({π΄} βͺ (π΄ β {π΅})) = (suc π΄ β {π΅})) | ||
Theorem | phplem2OLD 9095 | Obsolete lemma for php 9087. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΄ β V & β’ π΅ β V β β’ ((π΄ β Ο β§ π΅ β π΄) β π΄ β (suc π΄ β {π΅})) | ||
Theorem | phplem3OLD 9096 | Obsolete version of phplem1 9084 as of 23-Sep-2024. (Contributed by NM, 26-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΄ β V & β’ π΅ β V β β’ ((π΄ β Ο β§ π΅ β suc π΄) β π΄ β (suc π΄ β {π΅})) | ||
Theorem | phplem4OLD 9097 | Obsolete version of phplem2 9085 as of 4-Nov-2024. (Contributed by NM, 28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΄ β V & β’ π΅ β V β β’ ((π΄ β Ο β§ π΅ β Ο) β (suc π΄ β suc π΅ β π΄ β π΅)) | ||
Theorem | nneneqOLD 9098 | Obsolete version of nneneq 9086 as of 11-Nov-2024. (Contributed by NM, 28-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅ β π΄ = π΅)) | ||
Theorem | phpOLD 9099 | Obsolete version of php 9087 as of 18-Nov-2024. (Contributed by NM, 29-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β Β¬ π΄ β π΅) | ||
Theorem | php2OLD 9100 | Obsolete version of php2 9088 as of 20-Nov-2024. (Contributed by NM, 31-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ βΊ π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |