![]() |
Metamath
Proof Explorer Theorem List (p. 92 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 | 0domgOLD 9101 | Obsolete version of 0domg 9100 as of 29-Nov-2024. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β π β β βΌ π΄) | ||
Theorem | dom0 9102 | A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.) Avoid ax-pow 5364, ax-un 7725. (Revised by BTernaryTau, 29-Nov-2024.) |
β’ (π΄ βΌ β β π΄ = β ) | ||
Theorem | dom0OLD 9103 | Obsolete version of dom0 9102 as of 29-Nov-2024. (Contributed by NM, 22-Nov-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ βΌ β β π΄ = β ) | ||
Theorem | 0sdomg 9104 | A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006.) Avoid ax-pow 5364, ax-un 7725. (Revised by BTernaryTau, 29-Nov-2024.) |
β’ (π΄ β π β (β βΊ π΄ β π΄ β β )) | ||
Theorem | 0sdomgOLD 9105 | Obsolete version of 0sdomg 9104 as of 29-Nov-2024. (Contributed by NM, 23-Mar-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β π β (β βΊ π΄ β π΄ β β )) | ||
Theorem | 0dom 9106 | Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
β’ π΄ β V β β’ β βΌ π΄ | ||
Theorem | 0sdom 9107 | A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 29-Jul-2004.) |
β’ π΄ β V β β’ (β βΊ π΄ β π΄ β β ) | ||
Theorem | sdom0 9108 | The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003.) Avoid ax-pow 5364, ax-un 7725. (Revised by BTernaryTau, 29-Nov-2024.) |
β’ Β¬ π΄ βΊ β | ||
Theorem | sdom0OLD 9109 | Obsolete version of sdom0 9108 as of 29-Nov-2024. (Contributed by NM, 26-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ Β¬ π΄ βΊ β | ||
Theorem | sdomdomtr 9110 | Transitivity of strict dominance and dominance. Theorem 22(iii) of [Suppes] p. 97. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
β’ ((π΄ βΊ π΅ β§ π΅ βΌ πΆ) β π΄ βΊ πΆ) | ||
Theorem | sdomentr 9111 | Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. (Contributed by NM, 26-Oct-2003.) |
β’ ((π΄ βΊ π΅ β§ π΅ β πΆ) β π΄ βΊ πΆ) | ||
Theorem | domsdomtr 9112 | Transitivity of dominance and strict dominance. Theorem 22(ii) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
β’ ((π΄ βΌ π΅ β§ π΅ βΊ πΆ) β π΄ βΊ πΆ) | ||
Theorem | ensdomtr 9113 | Transitivity of equinumerosity and strict dominance. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
β’ ((π΄ β π΅ β§ π΅ βΊ πΆ) β π΄ βΊ πΆ) | ||
Theorem | sdomirr 9114 | Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97. (Contributed by NM, 4-Jun-1998.) |
β’ Β¬ π΄ βΊ π΄ | ||
Theorem | sdomtr 9115 | Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97. (Contributed by NM, 9-Jun-1998.) |
β’ ((π΄ βΊ π΅ β§ π΅ βΊ πΆ) β π΄ βΊ πΆ) | ||
Theorem | sdomn2lp 9116 | Strict dominance has no 2-cycle loops. (Contributed by NM, 6-May-2008.) |
β’ Β¬ (π΄ βΊ π΅ β§ π΅ βΊ π΄) | ||
Theorem | enen1 9117 | Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.) |
β’ (π΄ β π΅ β (π΄ β πΆ β π΅ β πΆ)) | ||
Theorem | enen2 9118 | Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.) |
β’ (π΄ β π΅ β (πΆ β π΄ β πΆ β π΅)) | ||
Theorem | domen1 9119 | Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.) |
β’ (π΄ β π΅ β (π΄ βΌ πΆ β π΅ βΌ πΆ)) | ||
Theorem | domen2 9120 | Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.) |
β’ (π΄ β π΅ β (πΆ βΌ π΄ β πΆ βΌ π΅)) | ||
Theorem | sdomen1 9121 | Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.) |
β’ (π΄ β π΅ β (π΄ βΊ πΆ β π΅ βΊ πΆ)) | ||
Theorem | sdomen2 9122 | Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.) |
β’ (π΄ β π΅ β (πΆ βΊ π΄ β πΆ βΊ π΅)) | ||
Theorem | domtriord 9123 | Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ βΌ π΅ β Β¬ π΅ βΊ π΄)) | ||
Theorem | sdomel 9124 | For ordinals, strict dominance implies membership. (Contributed by Mario Carneiro, 13-Jan-2013.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ βΊ π΅ β π΄ β π΅)) | ||
Theorem | sdomdif 9125 | The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013.) |
β’ (π΄ βΊ π΅ β (π΅ β π΄) β β ) | ||
Theorem | onsdominel 9126 | An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
β’ ((π΄ β On β§ π΅ β On β§ (π΄ β© πΆ) βΊ (π΅ β© πΆ)) β π΄ β π΅) | ||
Theorem | domunsn 9127 | Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π΄ βΊ π΅ β (π΄ βͺ {πΆ}) βΌ π΅) | ||
Theorem | fodomr 9128* | There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.) |
β’ ((β βΊ π΅ β§ π΅ βΌ π΄) β βπ π:π΄βontoβπ΅) | ||
Theorem | pwdom 9129 | Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ (π΄ βΌ π΅ β π« π΄ βΌ π« π΅) | ||
Theorem | canth2 9130 | 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 7362. This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994.) |
β’ π΄ β V β β’ π΄ βΊ π« π΄ | ||
Theorem | canth2g 9131 | 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 9132 | 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 9133 | No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.) |
β’ (π΄ β π β π« π« π΄ β π΄) | ||
Theorem | disjen 9134 | A stronger form of pwuninel 8260. We can use pwuninel 8260, 2pwuninel 9132 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 9135* | Existence version of disjen 9134. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ ((π΄ β π β§ π΅ β π) β βπ₯((π΄ β© π₯) = β β§ π₯ β π΅)) | ||
Theorem | domss2 9136 | A corollary of disjenex 9135. 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 9137* | A corollary of disjenex 9135. 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 9138* | Weakening of domssex2 9137 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 9139* | 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 9140 | 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 9141 | 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 9142 | 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 9143 | 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 9144* | Lemma for xpmapen 9145. (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 9145 | 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 9146 | 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 9147 | 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 9148 | 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 9149 | Set exponentiation dominates the base. (Contributed by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 17-Jul-2022.) |
β’ ((π΄ β π β§ π΅ β π β§ π΅ β β ) β π΄ βΌ (π΄ βm π΅)) | ||
Theorem | pwen 9150 | 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 9151* | Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ (π΄ β π΅ β {π₯ β£ (π₯ β π΄ β§ π₯ β πΆ)} β {π₯ β£ (π₯ β π΅ β§ π₯ β πΆ)}) | ||
Theorem | limenpsi 9152 | 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 9153 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ Lim π΄ β β’ (π΄ β π β π΄ β suc π΄) | ||
Theorem | limensuc 9154 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ ((π΄ β π β§ Lim π΄) β π΄ β suc π΄) | ||
Theorem | infensuc 9155 | 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 9156 | Lemma for rexdif1en 9158 and dif1en 9160. (Contributed by BTernaryTau, 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to avoid ax-un 7725. (Revised by BTernaryTau, 5-Jan-2025.) |
β’ (((πΉ β π β§ π΄ β π β§ π β On) β§ πΉ:π΄β1-1-ontoβsuc π) β (π΄ β {(β‘πΉβπ)}) β π) | ||
Theorem | dif1enlemOLD 9157 | Obsolete version of dif1enlem 9156 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 9158* | 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 7725. (Revised by BTernaryTau, 5-Jan-2025.) |
β’ ((π β On β§ π΄ β suc π) β βπ₯ β π΄ (π΄ β {π₯}) β π) | ||
Theorem | rexdif1enOLD 9159* | Obsolete version of rexdif1en 9158 as of 5-Jan-2025. (Contributed by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Ο β§ π΄ β suc π) β βπ₯ β π΄ (π΄ β {π₯}) β π) | ||
Theorem | dif1en 9160 | 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 5364. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.) |
β’ ((π β On β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | dif1ennn 9161 | If a set π΄ is equinumerous to the successor of a natural number π, then π΄ with an element removed is equinumerous to π. See also dif1ennnALT 9277. (Contributed by BTernaryTau, 6-Jan-2025.) |
β’ ((π β Ο β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | dif1enOLD 9162 | Obsolete version of dif1en 9160 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5364. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β Ο β§ π΄ β suc π β§ π β π΄) β (π΄ β {π}) β π) | ||
Theorem | findcard 9163* | 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 9164* | 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 5364. (Revised by BTernaryTau, 26-Aug-2024.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β Fin β (π β π)) β β’ (π΄ β Fin β π) | ||
Theorem | findcard2s 9165* | Variation of findcard2 9164 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 9166* | Deduction version of findcard2 9164. (Contributed by SO, 16-Jul-2018.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ βͺ {π§}) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π β π) & β’ ((π β§ (π¦ β π΄ β§ π§ β (π΄ β π¦))) β (π β π)) & β’ (π β π΄ β Fin) β β’ (π β π) | ||
Theorem | nnfi 9167 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5364. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ (π΄ β Ο β π΄ β Fin) | ||
Theorem | pssnn 9168* | 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 5364. (Revised by BTernaryTau, 31-Jul-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β βπ₯ β π΄ π΅ β π₯) | ||
Theorem | ssnnfi 9169 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | ssnnfiOLD 9170 | Obsolete version of ssnnfi 9169 as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | 0fin 9171 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
β’ β β Fin | ||
Theorem | unfi 9172 | 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 5364. (Revised by BTernaryTau, 7-Aug-2024.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) β Fin) | ||
Theorem | ssfi 9173 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5364, see ssfiALT 9174. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5364. (Revised by BTernaryTau, 12-Aug-2024.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | ssfiALT 9174 | Shorter proof of ssfi 9173 using ax-pow 5364. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β π΄) β π΅ β Fin) | ||
Theorem | imafi 9175 | Images of finite sets are finite. For a shorter proof using ax-pow 5364, see imafiALT 9345. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5364. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ ((Fun πΉ β§ π β Fin) β (πΉ β π) β Fin) | ||
Theorem | pwfir 9176 | 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 9177* | Lemma for pwfi 9178. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5364. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ πΉ = (π β π« π β¦ (π βͺ {π₯})) β β’ (π« π β Fin β π« (π βͺ {π₯}) β Fin) | ||
Theorem | pwfi 9178 | 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 5364. (Revised by BTernaryTau, 7-Sep-2024.) |
β’ (π΄ β Fin β π« π΄ β Fin) | ||
Theorem | diffi 9179 | If π΄ is finite, (π΄ β π΅) is finite. (Contributed by FL, 3-Aug-2009.) |
β’ (π΄ β Fin β (π΄ β π΅) β Fin) | ||
Theorem | cnvfi 9180 | If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) Avoid ax-pow 5364. (Revised by BTernaryTau, 9-Sep-2024.) |
β’ (π΄ β Fin β β‘π΄ β Fin) | ||
Theorem | fnfi 9181 | A version of fnex 7219 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 9182 | 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 8967). (Contributed by BTernaryTau, 8-Sep-2024.) |
β’ ((π΄ β Fin β§ πΉ:π΄β1-1-ontoβπ΅) β π΄ β π΅) | ||
Theorem | f1oenfirn 9183 | 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 9184 | 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 8968). (Contributed by BTernaryTau, 25-Sep-2024.) |
β’ ((π΅ β Fin β§ πΉ:π΄β1-1βπ΅) β π΄ βΌ π΅) | ||
Theorem | f1domfi2 9185 | 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 8965). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π β§ πΉ:π΄β1-1βπ΅) β π΄ βΌ π΅) | ||
Theorem | enreffi 9186 | Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg 8980). (Contributed by BTernaryTau, 8-Sep-2024.) |
β’ (π΄ β Fin β π΄ β π΄) | ||
Theorem | ensymfib 9187 | Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb 8998). (Contributed by BTernaryTau, 9-Sep-2024.) |
β’ (π΄ β Fin β (π΄ β π΅ β π΅ β π΄)) | ||
Theorem | entrfil 9188 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9002). (Contributed by BTernaryTau, 10-Sep-2024.) |
β’ ((π΄ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | enfii 9189 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5364. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ ((π΅ β Fin β§ π΄ β π΅) β π΄ β Fin) | ||
Theorem | enfi 9190 | Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5364, see enfiALT 9191. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5364. (Revised by BTernaryTau, 23-Sep-2024.) |
β’ (π΄ β π΅ β (π΄ β Fin β π΅ β Fin)) | ||
Theorem | enfiALT 9191 | Shorter proof of enfi 9190 using ax-pow 5364. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β π΅ β (π΄ β Fin β π΅ β Fin)) | ||
Theorem | domfi 9192 | 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 9193 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9002). (Contributed by BTernaryTau, 23-Sep-2024.) |
β’ ((π΅ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | entrfir 9194 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9002). (Contributed by BTernaryTau, 23-Sep-2024.) |
β’ ((πΆ β Fin β§ π΄ β π΅ β§ π΅ β πΆ) β π΄ β πΆ) | ||
Theorem | domtrfil 9195 | Transitivity of dominance relation when π΄ is finite, proved without using the Axiom of Power Sets (unlike domtr 9003). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | domtrfi 9196 | Transitivity of dominance relation when π΅ is finite, proved without using the Axiom of Power Sets (unlike domtr 9003). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΅ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | domtrfir 9197 | Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 9003). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((πΆ β Fin β§ π΄ βΌ π΅ β§ π΅ βΌ πΆ) β π΄ βΌ πΆ) | ||
Theorem | f1imaenfi 9198 | 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 9010). (Contributed by BTernaryTau, 29-Sep-2024.) |
β’ ((πΉ:π΄β1-1βπ΅ β§ πΆ β π΄ β§ πΆ β Fin) β (πΉ β πΆ) β πΆ) | ||
Theorem | ssdomfi 9199 | A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8996). (Contributed by BTernaryTau, 12-Nov-2024.) |
β’ (π΅ β Fin β (π΄ β π΅ β π΄ βΌ π΅)) | ||
Theorem | ssdomfi2 9200 | A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8996). (Contributed by BTernaryTau, 24-Nov-2024.) |
β’ ((π΄ β Fin β§ π΅ β π β§ π΄ β π΅) β π΄ βΌ π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |