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