![]() |
Metamath
Proof Explorer Theorem List (p. 92 of 475) | < 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-29964) |
![]() (29965-31487) |
![]() (31488-47412) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fodomr 9101* | There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.) |
β’ ((β βΊ π΅ β§ π΅ βΌ π΄) β βπ π:π΄βontoβπ΅) | ||
Theorem | pwdom 9102 | Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ (π΄ βΌ π΅ β π« π΄ βΌ π« π΅) | ||
Theorem | canth2 9103 | 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 7337. This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994.) |
β’ π΄ β V β β’ π΄ βΊ π« π΄ | ||
Theorem | canth2g 9104 | 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 9105 | 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 9106 | No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.) |
β’ (π΄ β π β π« π« π΄ β π΄) | ||
Theorem | disjen 9107 | A stronger form of pwuninel 8233. We can use pwuninel 8233, 2pwuninel 9105 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 9108* | Existence version of disjen 9107. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ ((π΄ β π β§ π΅ β π) β βπ₯((π΄ β© π₯) = β β§ π₯ β π΅)) | ||
Theorem | domss2 9109 | A corollary of disjenex 9108. 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 9110* | A corollary of disjenex 9108. 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 9111* | Weakening of domssex2 9110 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 9112* | 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 9113 | 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 9114 | 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 9115 | 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 9116 | 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 9117* | Lemma for xpmapen 9118. (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 9118 | 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 9119 | 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 9120 | 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 9121 | 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 9122 | Set exponentiation dominates the base. (Contributed by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 17-Jul-2022.) |
β’ ((π΄ β π β§ π΅ β π β§ π΅ β β ) β π΄ βΌ (π΄ βm π΅)) | ||
Theorem | pwen 9123 | 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 9124* | Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ (π΄ β π΅ β {π₯ β£ (π₯ β π΄ β§ π₯ β πΆ)} β {π₯ β£ (π₯ β π΅ β§ π₯ β πΆ)}) | ||
Theorem | limenpsi 9125 | 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 9126 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ Lim π΄ β β’ (π΄ β π β π΄ β suc π΄) | ||
Theorem | limensuc 9127 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ ((π΄ β π β§ Lim π΄) β π΄ β suc π΄) | ||
Theorem | infensuc 9128 | 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 9129 | Lemma for rexdif1en 9131 and dif1en 9133. (Contributed by BTernaryTau, 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to avoid ax-un 7699. (Revised by BTernaryTau, 5-Jan-2025.) |
β’ (((πΉ β π β§ π΄ β π β§ π β On) β§ πΉ:π΄β1-1-ontoβsuc π) β (π΄ β {(β‘πΉβπ)}) β π) | ||
Theorem | dif1enlemOLD 9130 | Obsolete version of dif1enlem 9129 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 9131* | 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 7699. (Revised by BTernaryTau, 5-Jan-2025.) |
β’ ((π β On β§ π΄ β suc π) β βπ₯ β π΄ (π΄ β {π₯}) β π) | ||
Theorem | rexdif1enOLD 9132* | Obsolete version of rexdif1en 9131 as of 5-Jan-2025. (Contributed by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Ο β§ π΄ β suc π) β βπ₯ β π΄ (π΄ β {π₯}) β π) | ||
Theorem | dif1en 9133 | 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 5347. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.) |
β’ ((π β On β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | dif1ennn 9134 | If a set π΄ is equinumerous to the successor of a natural number π, then π΄ with an element removed is equinumerous to π. See also dif1ennnALT 9250. (Contributed by BTernaryTau, 6-Jan-2025.) |
β’ ((π β Ο β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | dif1enOLD 9135 | Obsolete version of dif1en 9133 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5347. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Ο β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | findcard 9136* | 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 9137* | 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 5347. (Revised by BTernaryTau, 26-Aug-2024.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β Fin β (π β π)) β β’ (π΄ β Fin β π) | ||
Theorem | findcard2s 9138* | Variation of findcard2 9137 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 9139* | Deduction version of findcard2 9137. (Contributed by SO, 16-Jul-2018.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π β π) & β’ ((π β§ (π¦ β π΄ β§ π§ β (π΄ β π¦))) β (π β π)) & β’ (π β π΄ β Fin) β β’ (π β π) | ||
Theorem | nnfi 9140 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5347. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ (π΄ β Ο β π΄ β Fin) | ||
Theorem | pssnn 9141* | 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 5347. (Revised by BTernaryTau, 31-Jul-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β βπ₯ β π΄ π΅ β π₯) | ||
Theorem | ssnnfi 9142 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | ssnnfiOLD 9143 | Obsolete version of ssnnfi 9142 as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | 0fin 9144 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
β’ β β Fin | ||
Theorem | unfi 9145 | 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 5347. (Revised by BTernaryTau, 7-Aug-2024.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) β Fin) | ||
Theorem | ssfi 9146 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5347, see ssfiALT 9147. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5347. (Revised by BTernaryTau, 12-Aug-2024.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | ssfiALT 9147 | Shorter proof of ssfi 9146 using ax-pow 5347. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | imafi 9148 | Images of finite sets are finite. For a shorter proof using ax-pow 5347, see imafiALT 9318. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5347. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ ((Fun πΉ β§ π β Fin) β (πΉ β π) β Fin) | ||
Theorem | pwfir 9149 | 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 9150* | Lemma for pwfi 9151. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5347. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ πΉ = (π β π« π β¦ (π βͺ {π₯})) β β’ (π« π β Fin β π« (π βͺ {π₯}) β Fin) | ||
Theorem | pwfi 9151 | 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 5347. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ (π΄ β Fin β π« π΄ β Fin) | ||
Theorem | diffi 9152 | If π΄ is finite, (π΄ β π΅) is finite. (Contributed by FL, 3-Aug-2009.) |
β’ (π΄ β Fin β (π΄ β π΅) β Fin) | ||
Theorem | cnvfi 9153 | If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) Avoid ax-pow 5347. (Revised by BTernaryTau, 9-Sep-2024.) |
β’ (π΄ β Fin β β‘π΄ β Fin) | ||
Theorem | fnfi 9154 | A version of fnex 7194 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 9155 | 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 8940). (Contributed by BTernaryTau, 8-Sep-2024.) |
β’ ((π΄ β Fin β§ πΉ:π΄β1-1-ontoβπ΅) β π΄ β π΅) | ||
Theorem | f1oenfirn 9156 | 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 9157 | 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 8941). (Contributed by BTernaryTau, 25-Sep-2024.) |
β’ ((π΅ β Fin β§ πΉ:π΄β1-1βπ΅) β π΄ βΌ π΅) | ||
Theorem | f1domfi2 9158 | 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 8938). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π β§ πΉ:π΄β1-1βπ΅) β π΄ βΌ π΅) | ||
Theorem | enreffi 9159 | Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg 8953). (Contributed by BTernaryTau, 8-Sep-2024.) |
β’ (π΄ β Fin β π΄ β π΄) | ||
Theorem | ensymfib 9160 | Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb 8971). (Contributed by BTernaryTau, 9-Sep-2024.) |
β’ (π΄ β Fin β (π΄ β π΅ β π΅ β π΄)) | ||
Theorem | entrfil 9161 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8975). (Contributed by BTernaryTau, 10-Sep-2024.) |
β’ ((π΄ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | enfii 9162 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5347. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ ((π΅ β Fin β§ π΄ β π΅) β π΄ β Fin) | ||
Theorem | enfi 9163 | Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5347, see enfiALT 9164. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5347. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ (π΄ β π΅ β (π΄ β Fin β π΅ β Fin)) | ||
Theorem | enfiALT 9164 | Shorter proof of enfi 9163 using ax-pow 5347. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β π΅ β (π΄ β Fin β π΅ β Fin)) | ||
Theorem | domfi 9165 | 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 9166 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8975). (Contributed by BTernaryTau, 23-Sep-2024.) |
β’ ((π΅ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | entrfir 9167 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8975). (Contributed by BTernaryTau, 23-Sep-2024.) |
β’ ((πΆ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | domtrfil 9168 | Transitivity of dominance relation when π΄ is finite, proved without using the Axiom of Power Sets (unlike domtr 8976). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | domtrfi 9169 | Transitivity of dominance relation when π΅ is finite, proved without using the Axiom of Power Sets (unlike domtr 8976). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | domtrfir 9170 | Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 8976). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((πΆ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | f1imaenfi 9171 | 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 8983). (Contributed by BTernaryTau, 29-Sep-2024.) |
β’ ((πΉ:π΄β1-1βπ΅ β§ πΆ β π΄ β§ πΆ β Fin) β (πΉ β πΆ) β πΆ) | ||
Theorem | ssdomfi 9172 | A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8969). (Contributed by BTernaryTau, 12-Nov-2024.) |
β’ (π΅ β Fin β (π΄ β π΅ β π΄ βΌ π΅)) | ||
Theorem | ssdomfi2 9173 | A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8969). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π β§ π΄ β π΅) β π΄ βΌ π΅) | ||
Theorem | sbthfilem 9174* | Lemma for sbthfi 9175. (Contributed by BTernaryTau, 4-Nov-2024.) |
β’ π΄ β V & β’ π· = {π₯ β£ (π₯ β π΄ β§ (π β (π΅ β (π β π₯))) β (π΄ β π₯))} & β’ π» = ((π βΎ βͺ π·) βͺ (β‘π βΎ (π΄ β βͺ π·))) & β’ π΅ β V β β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ π΄) β π΄ β π΅) | ||
Theorem | sbthfi 9175 | Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 9066). (Contributed by BTernaryTau, 4-Nov-2024.) |
β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ π΄) β π΄ β π΅) | ||
Theorem | domnsymfi 9176 | 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 9072). (Contributed by BTernaryTau, 22-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅) β Β¬ π΅ βΊ π΄) | ||
Theorem | sdomdomtrfi 9177 | Transitivity of strict dominance and dominance when π΄ is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 9083). (Contributed by BTernaryTau, 25-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΊ π΅ β§ π΅ βΌ πΆ) β π΄ βΊ πΆ) | ||
Theorem | domsdomtrfi 9178 | Transitivity of dominance and strict dominance when π΄ is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 9085). (Contributed by BTernaryTau, 25-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅ β§ π΅ βΊ πΆ) β π΄ βΊ πΆ) | ||
Theorem | sucdom2 9179 | 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 5347. (Revised by BTernaryTau, 4-Dec-2024.) |
β’ (π΄ βΊ π΅ β suc π΄ βΌ π΅) | ||
Theorem | phplem1 9180 | 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 5347. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ ((π΄ β Ο β§ π΅ β suc π΄) β π΄ β (suc π΄ β {π΅})) | ||
Theorem | phplem2 9181 | 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 5347. (Revised by BTernaryTau, 4-Nov-2024.) |
β’ π΄ β V β β’ ((π΄ β Ο β§ π΅ β Ο) β (suc π΄ β suc π΅ β π΄ β π΅)) | ||
Theorem | nneneq 9182 | 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 5347. (Revised by BTernaryTau, 11-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅ β π΄ = π΅)) | ||
Theorem | php 9183 | 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 9180, phplem2 9181, nneneq 9182, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5347. (Revised by BTernaryTau, 18-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β Β¬ π΄ β π΅) | ||
Theorem | php2 9184 | Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5347. (Revised by BTernaryTau, 20-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ βΊ π΄) | ||
Theorem | php3 9185 | 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 5347. (Revised by BTernaryTau, 26-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ βΊ π΄) | ||
Theorem | php4 9186 | Corollary of the Pigeonhole Principle php 9183: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.) |
β’ (π΄ β Ο β π΄ βΊ suc π΄) | ||
Theorem | php5 9187 | Corollary of the Pigeonhole Principle php 9183: 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 9188 | Corollary of the Pigeonhole Principle using equality. Strengthening of php 9183 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow. (Revised by BTernaryTau, 28-Nov-2024.) |
β’ (π β π΄ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π΄ β π΅) β β’ (π β π΄ = π΅) | ||
Theorem | nndomog 9189 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9206 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9206. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5347. (Revised by BTernaryTau, 29-Nov-2024.) |
β’ ((π΄ β Ο β§ π΅ β On) β (π΄ βΌ π΅ β π΄ β π΅)) | ||
Theorem | phplem1OLD 9190 | Obsolete lemma for php 9183. (Contributed by NM, 25-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β ({π΄} βͺ (π΄ β {π΅})) = (suc π΄ β {π΅})) | ||
Theorem | phplem2OLD 9191 | Obsolete lemma for php 9183. (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 9192 | Obsolete version of phplem1 9180 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 9193 | Obsolete version of phplem2 9181 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 9194 | Obsolete version of nneneq 9182 as of 11-Nov-2024. (Contributed by NM, 28-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅ β π΄ = π΅)) | ||
Theorem | phpOLD 9195 | Obsolete version of php 9183 as of 18-Nov-2024. (Contributed by NM, 29-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β Β¬ π΄ β π΅) | ||
Theorem | php2OLD 9196 | Obsolete version of php2 9184 as of 20-Nov-2024. (Contributed by NM, 31-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ βΊ π΄) | ||
Theorem | php3OLD 9197 | Obsolete version of php3 9185 as of 26-Nov-2024. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ βΊ π΄) | ||
Theorem | phpeqdOLD 9198 | Obsolete version of phpeqd 9188 as of 28-Nov-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π΄ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π΄ β π΅) β β’ (π β π΄ = π΅) | ||
Theorem | nndomogOLD 9199 | Obsolete version of nndomog 9189 as of 29-Nov-2024. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9206. (Revised by RP, 5-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β On) β (π΄ βΌ π΅ β π΄ β π΅)) | ||
Theorem | snnen2oOLD 9200 | Obsolete version of snnen2o 9210 as of 18-Nov-2024. (Contributed by AV, 6-Aug-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ Β¬ {π΄} β 2o |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |