Home | Metamath
Proof Explorer Theorem List (p. 90 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | en1bOLD 8901 | Obsolete version of en1b 8900 as of 24-Sep-2024. (Contributed by Mario Carneiro, 17-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (๐ด โ 1o โ ๐ด = {โช ๐ด}) | ||
Theorem | reuen1 8902* | Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (โ!๐ฅ โ ๐ด ๐ โ {๐ฅ โ ๐ด โฃ ๐} โ 1o) | ||
Theorem | euen1 8903 | Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
โข (โ!๐ฅ๐ โ {๐ฅ โฃ ๐} โ 1o) | ||
Theorem | euen1b 8904* | Two ways to express "๐ด has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.) |
โข (๐ด โ 1o โ โ!๐ฅ ๐ฅ โ ๐ด) | ||
Theorem | en1uniel 8905 | A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.) Avoid ax-un 7662. (Revised by BTernaryTau, 24-Sep-2024.) |
โข (๐ โ 1o โ โช ๐ โ ๐) | ||
Theorem | en1unielOLD 8906 | Obsolete version of en1uniel 8905 as of 24-Sep-2024. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (๐ โ 1o โ โช ๐ โ ๐) | ||
Theorem | 2dom 8907* | A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.) |
โข (2o โผ ๐ด โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ยฌ ๐ฅ = ๐ฆ) | ||
Theorem | fundmen 8908 | A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 28-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
โข ๐น โ V โ โข (Fun ๐น โ dom ๐น โ ๐น) | ||
Theorem | fundmeng 8909 | A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.) |
โข ((๐น โ ๐ โง Fun ๐น) โ dom ๐น โ ๐น) | ||
Theorem | cnven 8910 | A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.) |
โข ((Rel ๐ด โง ๐ด โ ๐) โ ๐ด โ โก๐ด) | ||
Theorem | cnvct 8911 | If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
โข (๐ด โผ ฯ โ โก๐ด โผ ฯ) | ||
Theorem | fndmeng 8912 | A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข ((๐น Fn ๐ด โง ๐ด โ ๐ถ) โ ๐ด โ ๐น) | ||
Theorem | mapsnend 8913 | Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by Glauco Siliprandi, 24-Dec-2020.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) โ โข (๐ โ (๐ด โm {๐ต}) โ ๐ด) | ||
Theorem | mapsnen 8914 | Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Revised by Mario Carneiro, 15-Nov-2014.) (Proof shortened by AV, 17-Jul-2022.) |
โข ๐ด โ V & โข ๐ต โ V โ โข (๐ด โm {๐ต}) โ ๐ด | ||
Theorem | snmapen 8915 | Set exponentiation: a singleton to any set is equinumerous to that singleton. (Contributed by NM, 17-Dec-2003.) (Revised by AV, 17-Jul-2022.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ({๐ด} โm ๐ต) โ {๐ด}) | ||
Theorem | snmapen1 8916 | Set exponentiation: a singleton to any set is equinumerous to ordinal 1. (Proposed by BJ, 17-Jul-2022.) (Contributed by AV, 17-Jul-2022.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ({๐ด} โm ๐ต) โ 1o) | ||
Theorem | map1 8917 | Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1. Exercise 4.42(b) of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Proof shortened by AV, 17-Jul-2022.) |
โข (๐ด โ ๐ โ (1o โm ๐ด) โ 1o) | ||
Theorem | en2sn 8918 | Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5318. (Revised by BTernaryTau, 31-Jul-2024.) Avoid ax-un 7662. (Revised by BTernaryTau, 25-Sep-2024.) |
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ {๐ด} โ {๐ต}) | ||
Theorem | en2snOLD 8919 | Obsolete version of en2sn 8918 as of 25-Sep-2024. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5318. (Revised by BTernaryTau, 31-Jul-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ {๐ด} โ {๐ต}) | ||
Theorem | en2snOLDOLD 8920 | Obsolete version of en2sn 8918 as of 31-Jul-2024. (Contributed by NM, 9-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ {๐ด} โ {๐ต}) | ||
Theorem | snfi 8921 | A singleton is finite. (Contributed by NM, 4-Nov-2002.) |
โข {๐ด} โ Fin | ||
Theorem | fiprc 8922 | The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.) |
โข Fin โ V | ||
Theorem | unen 8923 | Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
โข (((๐ด โ ๐ต โง ๐ถ โ ๐ท) โง ((๐ด โฉ ๐ถ) = โ โง (๐ต โฉ ๐ท) = โ )) โ (๐ด โช ๐ถ) โ (๐ต โช ๐ท)) | ||
Theorem | enrefnn 8924 | Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg 8857). (Contributed by BTernaryTau, 31-Jul-2024.) |
โข (๐ด โ ฯ โ ๐ด โ ๐ด) | ||
Theorem | en2prd 8925 | Two unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข (๐ โ ๐ท โ ๐) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ถ โ ๐ท) โ โข (๐ โ {๐ด, ๐ต} โ {๐ถ, ๐ท}) | ||
Theorem | enpr2d 8926 | A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-un 7662. (Revised by BTernaryTau, 23-Dec-2024.) |
โข (๐ โ ๐ด โ ๐ถ) & โข (๐ โ ๐ต โ ๐ท) & โข (๐ โ ยฌ ๐ด = ๐ต) โ โข (๐ โ {๐ด, ๐ต} โ 2o) | ||
Theorem | enpr2dOLD 8927 | Obsolete version of enpr2d 8926 as of 23-Dec-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (๐ โ ๐ด โ ๐ถ) & โข (๐ โ ๐ต โ ๐ท) & โข (๐ โ ยฌ ๐ด = ๐ต) โ โข (๐ โ {๐ด, ๐ต} โ 2o) | ||
Theorem | ssct 8928 | Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017.) Avoid ax-pow 5318, ax-un 7662. (Revised by BTernaryTau, 7-Dec-2024.) |
โข ((๐ด โ ๐ต โง ๐ต โผ ฯ) โ ๐ด โผ ฯ) | ||
Theorem | ssctOLD 8929 | Obsolete version of ssct 8928 as of 7-Dec-2024. (Contributed by Thierry Arnoux, 31-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ((๐ด โ ๐ต โง ๐ต โผ ฯ) โ ๐ด โผ ฯ) | ||
Theorem | difsnen 8930 | All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
โข ((๐ โ ๐ โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐ โ {๐ด}) โ (๐ โ {๐ต})) | ||
Theorem | domdifsn 8931 | Dominance over a set with one element removed. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
โข (๐ด โบ ๐ต โ ๐ด โผ (๐ต โ {๐ถ})) | ||
Theorem | xpsnen 8932 | A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 4-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
โข ๐ด โ V & โข ๐ต โ V โ โข (๐ด ร {๐ต}) โ ๐ด | ||
Theorem | xpsneng 8933 | A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 22-Oct-2004.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด ร {๐ต}) โ ๐ด) | ||
Theorem | xp1en 8934 | One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
โข (๐ด โ ๐ โ (๐ด ร 1o) โ ๐ด) | ||
Theorem | endisj 8935* | Any two sets are equinumerous to two disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.) |
โข ๐ด โ V & โข ๐ต โ V โ โข โ๐ฅโ๐ฆ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ฅ โฉ ๐ฆ) = โ ) | ||
Theorem | undom 8936 | Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257. (Contributed by NM, 3-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-pow 5318. (Revised by BTernaryTau, 4-Dec-2024.) |
โข (((๐ด โผ ๐ต โง ๐ถ โผ ๐ท) โง (๐ต โฉ ๐ท) = โ ) โ (๐ด โช ๐ถ) โผ (๐ต โช ๐ท)) | ||
Theorem | undomOLD 8937 | Obsolete version of undom 8936 as of 4-Dec-2024. (Contributed by NM, 3-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (((๐ด โผ ๐ต โง ๐ถ โผ ๐ท) โง (๐ต โฉ ๐ท) = โ ) โ (๐ด โช ๐ถ) โผ (๐ต โช ๐ท)) | ||
Theorem | xpcomf1o 8938* | The canonical bijection from (๐ด ร ๐ต) to (๐ต ร ๐ด). (Contributed by Mario Carneiro, 23-Apr-2014.) |
โข ๐น = (๐ฅ โ (๐ด ร ๐ต) โฆ โช โก{๐ฅ}) โ โข ๐น:(๐ด ร ๐ต)โ1-1-ontoโ(๐ต ร ๐ด) | ||
Theorem | xpcomco 8939* | Composition with the bijection of xpcomf1o 8938 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.) |
โข ๐น = (๐ฅ โ (๐ด ร ๐ต) โฆ โช โก{๐ฅ}) & โข ๐บ = (๐ฆ โ ๐ต, ๐ง โ ๐ด โฆ ๐ถ) โ โข (๐บ โ ๐น) = (๐ง โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) | ||
Theorem | xpcomen 8940 | Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 5-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
โข ๐ด โ V & โข ๐ต โ V โ โข (๐ด ร ๐ต) โ (๐ต ร ๐ด) | ||
Theorem | xpcomeng 8941 | Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด ร ๐ต) โ (๐ต ร ๐ด)) | ||
Theorem | xpsnen2g 8942 | A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ({๐ด} ร ๐ต) โ ๐ต) | ||
Theorem | xpassen 8943 | Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by NM, 22-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
โข ๐ด โ V & โข ๐ต โ V & โข ๐ถ โ V โ โข ((๐ด ร ๐ต) ร ๐ถ) โ (๐ด ร (๐ต ร ๐ถ)) | ||
Theorem | xpdom2 8944 | Dominance law for Cartesian product. Proposition 10.33(2) of [TakeutiZaring] p. 92. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
โข ๐ถ โ V โ โข (๐ด โผ ๐ต โ (๐ถ ร ๐ด) โผ (๐ถ ร ๐ต)) | ||
Theorem | xpdom2g 8945 | Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.) |
โข ((๐ถ โ ๐ โง ๐ด โผ ๐ต) โ (๐ถ ร ๐ด) โผ (๐ถ ร ๐ต)) | ||
Theorem | xpdom1g 8946 | Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 25-Mar-2006.) (Revised by Mario Carneiro, 26-Apr-2015.) |
โข ((๐ถ โ ๐ โง ๐ด โผ ๐ต) โ (๐ด ร ๐ถ) โผ (๐ต ร ๐ถ)) | ||
Theorem | xpdom3 8947 | A set is dominated by its Cartesian product with a nonempty set. Exercise 6 of [Suppes] p. 98. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐ โง ๐ต โ โ ) โ ๐ด โผ (๐ด ร ๐ต)) | ||
Theorem | xpdom1 8948 | Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 28-Sep-2004.) (Revised by NM, 29-Mar-2006.) (Revised by Mario Carneiro, 7-May-2015.) |
โข ๐ถ โ V โ โข (๐ด โผ ๐ต โ (๐ด ร ๐ถ) โผ (๐ต ร ๐ถ)) | ||
Theorem | domunsncan 8949 | A singleton cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.) |
โข ๐ด โ V & โข ๐ต โ V โ โข ((ยฌ ๐ด โ ๐ โง ยฌ ๐ต โ ๐) โ (({๐ด} โช ๐) โผ ({๐ต} โช ๐) โ ๐ โผ ๐)) | ||
Theorem | omxpenlem 8950* | Lemma for omxpen 8951. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.) |
โข ๐น = (๐ฅ โ ๐ต, ๐ฆ โ ๐ด โฆ ((๐ด ยทo ๐ฅ) +o ๐ฆ)) โ โข ((๐ด โ On โง ๐ต โ On) โ ๐น:(๐ต ร ๐ด)โ1-1-ontoโ(๐ด ยทo ๐ต)) | ||
Theorem | omxpen 8951 | The cardinal and ordinal products are always equinumerous. Exercise 10 of [TakeutiZaring] p. 89. (Contributed by Mario Carneiro, 3-Mar-2013.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ (๐ด ร ๐ต)) | ||
Theorem | omf1o 8952* | Construct an explicit bijection from ๐ด ยทo ๐ต to ๐ต ยทo ๐ด. (Contributed by Mario Carneiro, 30-May-2015.) |
โข ๐น = (๐ฅ โ ๐ต, ๐ฆ โ ๐ด โฆ ((๐ด ยทo ๐ฅ) +o ๐ฆ)) & โข ๐บ = (๐ฅ โ ๐ต, ๐ฆ โ ๐ด โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) โ โข ((๐ด โ On โง ๐ต โ On) โ (๐บ โ โก๐น):(๐ด ยทo ๐ต)โ1-1-ontoโ(๐ต ยทo ๐ด)) | ||
Theorem | pw2f1olem 8953* | Lemma for pw2f1o 8954. (Contributed by Mario Carneiro, 6-Oct-2014.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข (๐ โ ๐ต โ ๐ถ) โ โข (๐ โ ((๐ โ ๐ซ ๐ด โง ๐บ = (๐ง โ ๐ด โฆ if(๐ง โ ๐, ๐ถ, ๐ต))) โ (๐บ โ ({๐ต, ๐ถ} โm ๐ด) โง ๐ = (โก๐บ โ {๐ถ})))) | ||
Theorem | pw2f1o 8954* | The power set of a set is equinumerous to set exponentiation with an unordered pair base of ordinal 2. Generalized from Proposition 10.44 of [TakeutiZaring] p. 96. (Contributed by Mario Carneiro, 6-Oct-2014.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข (๐ โ ๐ต โ ๐ถ) & โข ๐น = (๐ฅ โ ๐ซ ๐ด โฆ (๐ง โ ๐ด โฆ if(๐ง โ ๐ฅ, ๐ถ, ๐ต))) โ โข (๐ โ ๐น:๐ซ ๐ดโ1-1-ontoโ({๐ต, ๐ถ} โm ๐ด)) | ||
Theorem | pw2eng 8955 | The power set of a set is equinumerous to set exponentiation with a base of ordinal 2o. (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 1-Jul-2015.) |
โข (๐ด โ ๐ โ ๐ซ ๐ด โ (2o โm ๐ด)) | ||
Theorem | pw2en 8956 | The power set of a set is equinumerous to set exponentiation with a base of ordinal 2. Proposition 10.44 of [TakeutiZaring] p. 96. This is Metamath 100 proof #52. (Contributed by NM, 29-Jan-2004.) (Proof shortened by Mario Carneiro, 1-Jul-2015.) |
โข ๐ด โ V โ โข ๐ซ ๐ด โ (2o โm ๐ด) | ||
Theorem | fopwdom 8957 | Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) (Revised by AV, 18-Sep-2021.) |
โข ((๐น โ ๐ โง ๐น:๐ดโontoโ๐ต) โ ๐ซ ๐ต โผ ๐ซ ๐ด) | ||
Theorem | enfixsn 8958* | Given two equipollent sets, a bijection can always be chosen which fixes a single point. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
โข ((๐ด โ ๐ โง ๐ต โ ๐ โง ๐ โ ๐) โ โ๐(๐:๐โ1-1-ontoโ๐ โง (๐โ๐ด) = ๐ต)) | ||
Theorem | sucdom2OLD 8959 | Obsolete version of sucdom2 9083 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (๐ด โบ ๐ต โ suc ๐ด โผ ๐ต) | ||
Theorem | sbthlem1 8960* | Lemma for sbth 8970. (Contributed by NM, 22-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} โ โข โช ๐ท โ (๐ด โ (๐ โ (๐ต โ (๐ โ โช ๐ท)))) | ||
Theorem | sbthlem2 8961* | Lemma for sbth 8970. (Contributed by NM, 22-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} โ โข (ran ๐ โ ๐ด โ (๐ด โ (๐ โ (๐ต โ (๐ โ โช ๐ท)))) โ โช ๐ท) | ||
Theorem | sbthlem3 8962* | Lemma for sbth 8970. (Contributed by NM, 22-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} โ โข (ran ๐ โ ๐ด โ (๐ โ (๐ต โ (๐ โ โช ๐ท))) = (๐ด โ โช ๐ท)) | ||
Theorem | sbthlem4 8963* | Lemma for sbth 8970. (Contributed by NM, 27-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} โ โข (((dom ๐ = ๐ต โง ran ๐ โ ๐ด) โง Fun โก๐) โ (โก๐ โ (๐ด โ โช ๐ท)) = (๐ต โ (๐ โ โช ๐ท))) | ||
Theorem | sbthlem5 8964* | Lemma for sbth 8970. (Contributed by NM, 22-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} & โข ๐ป = ((๐ โพ โช ๐ท) โช (โก๐ โพ (๐ด โ โช ๐ท))) โ โข ((dom ๐ = ๐ด โง ran ๐ โ ๐ด) โ dom ๐ป = ๐ด) | ||
Theorem | sbthlem6 8965* | Lemma for sbth 8970. (Contributed by NM, 27-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} & โข ๐ป = ((๐ โพ โช ๐ท) โช (โก๐ โพ (๐ด โ โช ๐ท))) โ โข ((ran ๐ โ ๐ต โง ((dom ๐ = ๐ต โง ran ๐ โ ๐ด) โง Fun โก๐)) โ ran ๐ป = ๐ต) | ||
Theorem | sbthlem7 8966* | Lemma for sbth 8970. (Contributed by NM, 27-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} & โข ๐ป = ((๐ โพ โช ๐ท) โช (โก๐ โพ (๐ด โ โช ๐ท))) โ โข ((Fun ๐ โง Fun โก๐) โ Fun ๐ป) | ||
Theorem | sbthlem8 8967* | Lemma for sbth 8970. (Contributed by NM, 27-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} & โข ๐ป = ((๐ โพ โช ๐ท) โช (โก๐ โพ (๐ด โ โช ๐ท))) โ โข ((Fun โก๐ โง (((Fun ๐ โง dom ๐ = ๐ต) โง ran ๐ โ ๐ด) โง Fun โก๐)) โ Fun โก๐ป) | ||
Theorem | sbthlem9 8968* | Lemma for sbth 8970. (Contributed by NM, 28-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} & โข ๐ป = ((๐ โพ โช ๐ท) โช (โก๐ โพ (๐ด โ โช ๐ท))) โ โข ((๐:๐ดโ1-1โ๐ต โง ๐:๐ตโ1-1โ๐ด) โ ๐ป:๐ดโ1-1-ontoโ๐ต) | ||
Theorem | sbthlem10 8969* | Lemma for sbth 8970. (Contributed by NM, 28-Mar-1998.) |
โข ๐ด โ V & โข ๐ท = {๐ฅ โฃ (๐ฅ โ ๐ด โง (๐ โ (๐ต โ (๐ โ ๐ฅ))) โ (๐ด โ ๐ฅ))} & โข ๐ป = ((๐ โพ โช ๐ท) โช (โก๐ โพ (๐ด โ โช ๐ท))) & โข ๐ต โ V โ โข ((๐ด โผ ๐ต โง ๐ต โผ ๐ด) โ ๐ด โ ๐ต) | ||
Theorem | sbth 8970 |
Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This
theorem states that if set ๐ด is smaller (has lower cardinality)
than
๐ต and vice-versa, then ๐ด and
๐ต
are equinumerous (have the
same cardinality). The interesting thing is that this can be proved
without invoking the Axiom of Choice, as we do here. The theorem can
also be proved from the axiom of choice and the linear order of the
cardinal numbers, but our development does not provide the linear order
of cardinal numbers until much later and in ways that depend on
Schroeder-Bernstein.
The main proof consists of lemmas sbthlem1 8960 through sbthlem10 8969; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 8969. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level. Note that Suppes' proof, which is credited to J. M. Whitaker, does not require the Axiom of Infinity. In the Intuitionistic Logic Explorer (ILE) the Schroeder-Bernstein Theorem has been proven equivalent to the law of the excluded middle (LEM), and in ILE the LEM is not accepted as necessarily true; see https://us.metamath.org/ileuni/exmidsbth.html 8969. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.) |
โข ((๐ด โผ ๐ต โง ๐ต โผ ๐ด) โ ๐ด โ ๐ต) | ||
Theorem | sbthb 8971 | Schroeder-Bernstein Theorem and its converse. (Contributed by NM, 8-Jun-1998.) |
โข ((๐ด โผ ๐ต โง ๐ต โผ ๐ด) โ ๐ด โ ๐ต) | ||
Theorem | sbthcl 8972 | Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998.) |
โข โ = ( โผ โฉ โก โผ ) | ||
Theorem | dfsdom2 8973 | Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.) |
โข โบ = ( โผ โ โก โผ ) | ||
Theorem | brsdom2 8974 | Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97. (Contributed by NM, 27-Jul-2004.) |
โข ๐ด โ V & โข ๐ต โ V โ โข (๐ด โบ ๐ต โ (๐ด โผ ๐ต โง ยฌ ๐ต โผ ๐ด)) | ||
Theorem | sdomnsym 8975 | Strict dominance is asymmetric. Theorem 21(ii) of [Suppes] p. 97. (Contributed by NM, 8-Jun-1998.) |
โข (๐ด โบ ๐ต โ ยฌ ๐ต โบ ๐ด) | ||
Theorem | domnsym 8976 | Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.) |
โข (๐ด โผ ๐ต โ ยฌ ๐ต โบ ๐ด) | ||
Theorem | 0domg 8977 | Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-pow 5318, ax-un 7662. (Revised by BTernaryTau, 29-Nov-2024.) |
โข (๐ด โ ๐ โ โ โผ ๐ด) | ||
Theorem | 0domgOLD 8978 | Obsolete version of 0domg 8977 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 8979 | A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.) Avoid ax-pow 5318, ax-un 7662. (Revised by BTernaryTau, 29-Nov-2024.) |
โข (๐ด โผ โ โ ๐ด = โ ) | ||
Theorem | dom0OLD 8980 | Obsolete version of dom0 8979 as of 29-Nov-2024. (Contributed by NM, 22-Nov-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (๐ด โผ โ โ ๐ด = โ ) | ||
Theorem | 0sdomg 8981 | A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006.) Avoid ax-pow 5318, ax-un 7662. (Revised by BTernaryTau, 29-Nov-2024.) |
โข (๐ด โ ๐ โ (โ โบ ๐ด โ ๐ด โ โ )) | ||
Theorem | 0sdomgOLD 8982 | Obsolete version of 0sdomg 8981 as of 29-Nov-2024. (Contributed by NM, 23-Mar-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (๐ด โ ๐ โ (โ โบ ๐ด โ ๐ด โ โ )) | ||
Theorem | 0dom 8983 | Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
โข ๐ด โ V โ โข โ โผ ๐ด | ||
Theorem | 0sdom 8984 | A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 29-Jul-2004.) |
โข ๐ด โ V โ โข (โ โบ ๐ด โ ๐ด โ โ ) | ||
Theorem | sdom0 8985 | The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003.) Avoid ax-pow 5318, ax-un 7662. (Revised by BTernaryTau, 29-Nov-2024.) |
โข ยฌ ๐ด โบ โ | ||
Theorem | sdom0OLD 8986 | Obsolete version of sdom0 8985 as of 29-Nov-2024. (Contributed by NM, 26-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ยฌ ๐ด โบ โ | ||
Theorem | sdomdomtr 8987 | 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 8988 | Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. (Contributed by NM, 26-Oct-2003.) |
โข ((๐ด โบ ๐ต โง ๐ต โ ๐ถ) โ ๐ด โบ ๐ถ) | ||
Theorem | domsdomtr 8989 | 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 8990 | Transitivity of equinumerosity and strict dominance. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
โข ((๐ด โ ๐ต โง ๐ต โบ ๐ถ) โ ๐ด โบ ๐ถ) | ||
Theorem | sdomirr 8991 | Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97. (Contributed by NM, 4-Jun-1998.) |
โข ยฌ ๐ด โบ ๐ด | ||
Theorem | sdomtr 8992 | Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97. (Contributed by NM, 9-Jun-1998.) |
โข ((๐ด โบ ๐ต โง ๐ต โบ ๐ถ) โ ๐ด โบ ๐ถ) | ||
Theorem | sdomn2lp 8993 | Strict dominance has no 2-cycle loops. (Contributed by NM, 6-May-2008.) |
โข ยฌ (๐ด โบ ๐ต โง ๐ต โบ ๐ด) | ||
Theorem | enen1 8994 | Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.) |
โข (๐ด โ ๐ต โ (๐ด โ ๐ถ โ ๐ต โ ๐ถ)) | ||
Theorem | enen2 8995 | Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.) |
โข (๐ด โ ๐ต โ (๐ถ โ ๐ด โ ๐ถ โ ๐ต)) | ||
Theorem | domen1 8996 | Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.) |
โข (๐ด โ ๐ต โ (๐ด โผ ๐ถ โ ๐ต โผ ๐ถ)) | ||
Theorem | domen2 8997 | Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.) |
โข (๐ด โ ๐ต โ (๐ถ โผ ๐ด โ ๐ถ โผ ๐ต)) | ||
Theorem | sdomen1 8998 | Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.) |
โข (๐ด โ ๐ต โ (๐ด โบ ๐ถ โ ๐ต โบ ๐ถ)) | ||
Theorem | sdomen2 8999 | Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.) |
โข (๐ด โ ๐ต โ (๐ถ โบ ๐ด โ ๐ถ โบ ๐ต)) | ||
Theorem | domtriord 9000 | Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009.) |
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โผ ๐ต โ ยฌ ๐ต โบ ๐ด)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |