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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | domtriord 9001 | Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ βΌ π΅ β Β¬ π΅ βΊ π΄)) | ||
Theorem | sdomel 9002 | For ordinals, strict dominance implies membership. (Contributed by Mario Carneiro, 13-Jan-2013.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ βΊ π΅ β π΄ β π΅)) | ||
Theorem | sdomdif 9003 | The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013.) |
β’ (π΄ βΊ π΅ β (π΅ β π΄) β β ) | ||
Theorem | onsdominel 9004 | An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
β’ ((π΄ β On β§ π΅ β On β§ (π΄ β© πΆ) βΊ (π΅ β© πΆ)) β π΄ β π΅) | ||
Theorem | domunsn 9005 | Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π΄ βΊ π΅ β (π΄ βͺ {πΆ}) βΌ π΅) | ||
Theorem | fodomr 9006* | There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.) |
β’ ((β βΊ π΅ β§ π΅ βΌ π΄) β βπ π:π΄βontoβπ΅) | ||
Theorem | pwdom 9007 | Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ (π΄ βΌ π΅ β π« π΄ βΌ π« π΅) | ||
Theorem | canth2 9008 | 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 7303. This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994.) |
β’ π΄ β V β β’ π΄ βΊ π« π΄ | ||
Theorem | canth2g 9009 | 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 9010 | 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 9011 | No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.) |
β’ (π΄ β π β π« π« π΄ β π΄) | ||
Theorem | disjen 9012 | A stronger form of pwuninel 8174. We can use pwuninel 8174, 2pwuninel 9010 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 9013* | Existence version of disjen 9012. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ ((π΄ β π β§ π΅ β π) β βπ₯((π΄ β© π₯) = β β§ π₯ β π΅)) | ||
Theorem | domss2 9014 | A corollary of disjenex 9013. 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 9015* | A corollary of disjenex 9013. 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 9016* | Weakening of domssex2 9015 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 9017* | 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 9018 | 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 9019 | 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 9020 | 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 9021 | 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 9022* | Lemma for xpmapen 9023. (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 9023 | 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 9024 | 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 9025 | 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 9026 | 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 9027 | Set exponentiation dominates the base. (Contributed by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 17-Jul-2022.) |
β’ ((π΄ β π β§ π΅ β π β§ π΅ β β ) β π΄ βΌ (π΄ βm π΅)) | ||
Theorem | pwen 9028 | 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 9029* | Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ (π΄ β π΅ β {π₯ β£ (π₯ β π΄ β§ π₯ β πΆ)} β {π₯ β£ (π₯ β π΅ β§ π₯ β πΆ)}) | ||
Theorem | limenpsi 9030 | 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 9031 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ Lim π΄ β β’ (π΄ β π β π΄ β suc π΄) | ||
Theorem | limensuc 9032 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ ((π΄ β π β§ Lim π΄) β π΄ β suc π΄) | ||
Theorem | infensuc 9033 | 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 9034 | Lemma for rexdif1en 9036 and dif1en 9038. (Contributed by BTernaryTau, 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to avoid ax-un 7663. (Revised by BTernaryTau, 5-Jan-2025.) |
β’ (((πΉ β π β§ π΄ β π β§ π β On) β§ πΉ:π΄β1-1-ontoβsuc π) β (π΄ β {(β‘πΉβπ)}) β π) | ||
Theorem | dif1enlemOLD 9035 | Obsolete version of dif1enlem 9034 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 9036* | 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 7663. (Revised by BTernaryTau, 5-Jan-2025.) |
β’ ((π β On β§ π΄ β suc π) β βπ₯ β π΄ (π΄ β {π₯}) β π) | ||
Theorem | rexdif1enOLD 9037* | Obsolete version of rexdif1en 9036 as of 5-Jan-2025. (Contributed by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Ο β§ π΄ β suc π) β βπ₯ β π΄ (π΄ β {π₯}) β π) | ||
Theorem | dif1en 9038 | 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 5319. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.) |
β’ ((π β On β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | dif1ennn 9039 | If a set π΄ is equinumerous to the successor of a natural number π, then π΄ with an element removed is equinumerous to π. See also dif1ennnALT 9155. (Contributed by BTernaryTau, 6-Jan-2025.) |
β’ ((π β Ο β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | dif1enOLD 9040 | Obsolete version of dif1en 9038 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5319. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Ο β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | findcard 9041* | 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 9042* | 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 5319. (Revised by BTernaryTau, 26-Aug-2024.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β Fin β (π β π)) β β’ (π΄ β Fin β π) | ||
Theorem | findcard2s 9043* | Variation of findcard2 9042 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 9044* | Deduction version of findcard2 9042. (Contributed by SO, 16-Jul-2018.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π β π) & β’ ((π β§ (π¦ β π΄ β§ π§ β (π΄ β π¦))) β (π β π)) & β’ (π β π΄ β Fin) β β’ (π β π) | ||
Theorem | nnfi 9045 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5319. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ (π΄ β Ο β π΄ β Fin) | ||
Theorem | pssnn 9046* | 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 5319. (Revised by BTernaryTau, 31-Jul-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β βπ₯ β π΄ π΅ β π₯) | ||
Theorem | ssnnfi 9047 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | ssnnfiOLD 9048 | Obsolete version of ssnnfi 9047 as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | 0fin 9049 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
β’ β β Fin | ||
Theorem | unfi 9050 | 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 5319. (Revised by BTernaryTau, 7-Aug-2024.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) β Fin) | ||
Theorem | ssfi 9051 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5319, see ssfiALT 9052. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5319. (Revised by BTernaryTau, 12-Aug-2024.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | ssfiALT 9052 | Shorter proof of ssfi 9051 using ax-pow 5319. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | imafi 9053 | Images of finite sets are finite. For a shorter proof using ax-pow 5319, see imafiALT 9223. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ ((Fun πΉ β§ π β Fin) β (πΉ β π) β Fin) | ||
Theorem | pwfir 9054 | 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 9055* | Lemma for pwfi 9056. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ πΉ = (π β π« π β¦ (π βͺ {π₯})) β β’ (π« π β Fin β π« (π βͺ {π₯}) β Fin) | ||
Theorem | pwfi 9056 | 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 5319. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ (π΄ β Fin β π« π΄ β Fin) | ||
Theorem | diffi 9057 | If π΄ is finite, (π΄ β π΅) is finite. (Contributed by FL, 3-Aug-2009.) |
β’ (π΄ β Fin β (π΄ β π΅) β Fin) | ||
Theorem | cnvfi 9058 | If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) Avoid ax-pow 5319. (Revised by BTernaryTau, 9-Sep-2024.) |
β’ (π΄ β Fin β β‘π΄ β Fin) | ||
Theorem | fnfi 9059 | A version of fnex 7162 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 9060 | 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 8845). (Contributed by BTernaryTau, 8-Sep-2024.) |
β’ ((π΄ β Fin β§ πΉ:π΄β1-1-ontoβπ΅) β π΄ β π΅) | ||
Theorem | f1oenfirn 9061 | 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 9062 | 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 8846). (Contributed by BTernaryTau, 25-Sep-2024.) |
β’ ((π΅ β Fin β§ πΉ:π΄β1-1βπ΅) β π΄ βΌ π΅) | ||
Theorem | f1domfi2 9063 | 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 8843). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π β§ πΉ:π΄β1-1βπ΅) β π΄ βΌ π΅) | ||
Theorem | enreffi 9064 | Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg 8858). (Contributed by BTernaryTau, 8-Sep-2024.) |
β’ (π΄ β Fin β π΄ β π΄) | ||
Theorem | ensymfib 9065 | Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb 8876). (Contributed by BTernaryTau, 9-Sep-2024.) |
β’ (π΄ β Fin β (π΄ β π΅ β π΅ β π΄)) | ||
Theorem | entrfil 9066 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8880). (Contributed by BTernaryTau, 10-Sep-2024.) |
β’ ((π΄ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | enfii 9067 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5319. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ ((π΅ β Fin β§ π΄ β π΅) β π΄ β Fin) | ||
Theorem | enfi 9068 | Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5319, see enfiALT 9069. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5319. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ (π΄ β π΅ β (π΄ β Fin β π΅ β Fin)) | ||
Theorem | enfiALT 9069 | Shorter proof of enfi 9068 using ax-pow 5319. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β π΅ β (π΄ β Fin β π΅ β Fin)) | ||
Theorem | domfi 9070 | 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 9071 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8880). (Contributed by BTernaryTau, 23-Sep-2024.) |
β’ ((π΅ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | entrfir 9072 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8880). (Contributed by BTernaryTau, 23-Sep-2024.) |
β’ ((πΆ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | domtrfil 9073 | Transitivity of dominance relation when π΄ is finite, proved without using the Axiom of Power Sets (unlike domtr 8881). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | domtrfi 9074 | Transitivity of dominance relation when π΅ is finite, proved without using the Axiom of Power Sets (unlike domtr 8881). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | domtrfir 9075 | Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 8881). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((πΆ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | f1imaenfi 9076 | 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 8888). (Contributed by BTernaryTau, 29-Sep-2024.) |
β’ ((πΉ:π΄β1-1βπ΅ β§ πΆ β π΄ β§ πΆ β Fin) β (πΉ β πΆ) β πΆ) | ||
Theorem | ssdomfi 9077 | A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8874). (Contributed by BTernaryTau, 12-Nov-2024.) |
β’ (π΅ β Fin β (π΄ β π΅ β π΄ βΌ π΅)) | ||
Theorem | ssdomfi2 9078 | A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8874). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π β§ π΄ β π΅) β π΄ βΌ π΅) | ||
Theorem | sbthfilem 9079* | Lemma for sbthfi 9080. (Contributed by BTernaryTau, 4-Nov-2024.) |
β’ π΄ β V & β’ π· = {π₯ β£ (π₯ β π΄ β§ (π β (π΅ β (π β π₯))) β (π΄ β π₯))} & β’ π» = ((π βΎ βͺ π·) βͺ (β‘π βΎ (π΄ β βͺ π·))) & β’ π΅ β V β β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ π΄) β π΄ β π΅) | ||
Theorem | sbthfi 9080 | Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 8971). (Contributed by BTernaryTau, 4-Nov-2024.) |
β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ π΄) β π΄ β π΅) | ||
Theorem | domnsymfi 9081 | 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 8977). (Contributed by BTernaryTau, 22-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅) β Β¬ π΅ βΊ π΄) | ||
Theorem | sdomdomtrfi 9082 | Transitivity of strict dominance and dominance when π΄ is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 8988). (Contributed by BTernaryTau, 25-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΊ π΅ β§ π΅ βΌ πΆ) β π΄ βΊ πΆ) | ||
Theorem | domsdomtrfi 9083 | Transitivity of dominance and strict dominance when π΄ is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 8990). (Contributed by BTernaryTau, 25-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅ β§ π΅ βΊ πΆ) β π΄ βΊ πΆ) | ||
Theorem | sucdom2 9084 | 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 5319. (Revised by BTernaryTau, 4-Dec-2024.) |
β’ (π΄ βΊ π΅ β suc π΄ βΌ π΅) | ||
Theorem | phplem1 9085 | 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 5319. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ ((π΄ β Ο β§ π΅ β suc π΄) β π΄ β (suc π΄ β {π΅})) | ||
Theorem | phplem2 9086 | 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 5319. (Revised by BTernaryTau, 4-Nov-2024.) |
β’ π΄ β V β β’ ((π΄ β Ο β§ π΅ β Ο) β (suc π΄ β suc π΅ β π΄ β π΅)) | ||
Theorem | nneneq 9087 | 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 5319. (Revised by BTernaryTau, 11-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅ β π΄ = π΅)) | ||
Theorem | php 9088 | 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 9085, phplem2 9086, nneneq 9087, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5319. (Revised by BTernaryTau, 18-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β Β¬ π΄ β π΅) | ||
Theorem | php2 9089 | Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5319. (Revised by BTernaryTau, 20-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ βΊ π΄) | ||
Theorem | php3 9090 | 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 5319. (Revised by BTernaryTau, 26-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ βΊ π΄) | ||
Theorem | php4 9091 | Corollary of the Pigeonhole Principle php 9088: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.) |
β’ (π΄ β Ο β π΄ βΊ suc π΄) | ||
Theorem | php5 9092 | Corollary of the Pigeonhole Principle php 9088: 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 9093 | Corollary of the Pigeonhole Principle using equality. Strengthening of php 9088 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow. (Revised by BTernaryTau, 28-Nov-2024.) |
β’ (π β π΄ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π΄ β π΅) β β’ (π β π΄ = π΅) | ||
Theorem | nndomog 9094 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9111 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9111. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5319. (Revised by BTernaryTau, 29-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β On) β (π΄ βΌ π΅ β π΄ β π΅)) | ||
Theorem | phplem1OLD 9095 | Obsolete lemma for php 9088. (Contributed by NM, 25-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β ({π΄} βͺ (π΄ β {π΅})) = (suc π΄ β {π΅})) | ||
Theorem | phplem2OLD 9096 | Obsolete lemma for php 9088. (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 9097 | Obsolete version of phplem1 9085 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 9098 | Obsolete version of phplem2 9086 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 9099 | Obsolete version of nneneq 9087 as of 11-Nov-2024. (Contributed by NM, 28-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅ β π΄ = π΅)) | ||
Theorem | phpOLD 9100 | Obsolete version of php 9088 as of 18-Nov-2024. (Contributed by NM, 29-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β Β¬ π΄ β π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |