![]() |
Metamath
Proof Explorer Theorem List (p. 100 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-inr 9901 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
β’ inr = (π₯ β V β¦ β¨1o, π₯β©) | ||
Theorem | djueq12 9902 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ ((π΄ = π΅ β§ πΆ = π·) β (π΄ β πΆ) = (π΅ β π·)) | ||
Theorem | djueq1 9903 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ (π΄ = π΅ β (π΄ β πΆ) = (π΅ β πΆ)) | ||
Theorem | djueq2 9904 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ (π΄ = π΅ β (πΆ β π΄) = (πΆ β π΅)) | ||
Theorem | nfdju 9905 | Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯(π΄ β π΅) | ||
Theorem | djuex 9906 | The disjoint union of sets is a set. For a shorter proof using djuss 9918 see djuexALT 9920. (Contributed by AV, 28-Jun-2022.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ β π΅) β V) | ||
Theorem | djuexb 9907 | The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.) |
β’ ((π΄ β V β§ π΅ β V) β (π΄ β π΅) β V) | ||
Theorem | djulcl 9908 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
β’ (πΆ β π΄ β (inlβπΆ) β (π΄ β π΅)) | ||
Theorem | djurcl 9909 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
β’ (πΆ β π΅ β (inrβπΆ) β (π΄ β π΅)) | ||
Theorem | djulf1o 9910 | The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
β’ inl:Vβ1-1-ontoβ({β } Γ V) | ||
Theorem | djurf1o 9911 | The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
β’ inr:Vβ1-1-ontoβ({1o} Γ V) | ||
Theorem | inlresf 9912 | The left injection restricted to the left class of a disjoint union is a function from the left class into the disjoint union. (Contributed by AV, 27-Jun-2022.) |
β’ (inl βΎ π΄):π΄βΆ(π΄ β π΅) | ||
Theorem | inlresf1 9913 | The left injection restricted to the left class of a disjoint union is an injective function from the left class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
β’ (inl βΎ π΄):π΄β1-1β(π΄ β π΅) | ||
Theorem | inrresf 9914 | The right injection restricted to the right class of a disjoint union is a function from the right class into the disjoint union. (Contributed by AV, 27-Jun-2022.) |
β’ (inr βΎ π΅):π΅βΆ(π΄ β π΅) | ||
Theorem | inrresf1 9915 | The right injection restricted to the right class of a disjoint union is an injective function from the right class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
β’ (inr βΎ π΅):π΅β1-1β(π΄ β π΅) | ||
Theorem | djuin 9916 | The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) |
β’ ((inl β π΄) β© (inr β π΅)) = β | ||
Theorem | djur 9917* | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ (πΆ β (π΄ β π΅) β (βπ₯ β π΄ πΆ = (inlβπ₯) β¨ βπ₯ β π΅ πΆ = (inrβπ₯))) | ||
Theorem | djuss 9918 | A disjoint union is a subclass of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
β’ (π΄ β π΅) β ({β , 1o} Γ (π΄ βͺ π΅)) | ||
Theorem | djuunxp 9919 | The union of a disjoint union and its inversion is the Cartesian product of an unordered pair and the union of the left and right classes of the disjoint unions. (Proposed by GL, 4-Jul-2022.) (Contributed by AV, 4-Jul-2022.) |
β’ ((π΄ β π΅) βͺ (π΅ β π΄)) = ({β , 1o} Γ (π΄ βͺ π΅)) | ||
Theorem | djuexALT 9920 | Alternate proof of djuex 9906, which is shorter, but based indirectly on the definitions of inl and inr. (Proposed by BJ, 28-Jun-2022.) (Contributed by AV, 28-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ β π΅) β V) | ||
Theorem | eldju1st 9921 | The first component of an element of a disjoint union is either β or 1o. (Contributed by AV, 26-Jun-2022.) |
β’ (π β (π΄ β π΅) β ((1st βπ) = β β¨ (1st βπ) = 1o)) | ||
Theorem | eldju2ndl 9922 | The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.) |
β’ ((π β (π΄ β π΅) β§ (1st βπ) = β ) β (2nd βπ) β π΄) | ||
Theorem | eldju2ndr 9923 | The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.) |
β’ ((π β (π΄ β π΅) β§ (1st βπ) β β ) β (2nd βπ) β π΅) | ||
Theorem | djuun 9924 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) |
β’ ((inl β π΄) βͺ (inr β π΅)) = (π΄ β π΅) | ||
Theorem | 1stinl 9925 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (1st β(inlβπ)) = β ) | ||
Theorem | 2ndinl 9926 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (2nd β(inlβπ)) = π) | ||
Theorem | 1stinr 9927 | The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (1st β(inrβπ)) = 1o) | ||
Theorem | 2ndinr 9928 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (2nd β(inrβπ)) = π) | ||
Theorem | updjudhf 9929* | The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.) |
β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπΆ) & β’ π» = (π₯ β (π΄ β π΅) β¦ if((1st βπ₯) = β , (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯)))) β β’ (π β π»:(π΄ β π΅)βΆπΆ) | ||
Theorem | updjudhcoinlf 9930* | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.) |
β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπΆ) & β’ π» = (π₯ β (π΄ β π΅) β¦ if((1st βπ₯) = β , (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯)))) β β’ (π β (π» β (inl βΎ π΄)) = πΉ) | ||
Theorem | updjudhcoinrg 9931* | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.) |
β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπΆ) & β’ π» = (π₯ β (π΄ β π΅) β¦ if((1st βπ₯) = β , (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯)))) β β’ (π β (π» β (inr βΎ π΅)) = πΊ) | ||
Theorem | updjud 9932* | Universal property of the disjoint union. This theorem shows that the disjoint union, together with the left and right injections df-inl 9900 and df-inr 9901, is the coproduct in the category of sets, see Wikipedia "Coproduct", https://en.wikipedia.org/wiki/Coproduct 9901 (25-Aug-2023). This is a special case of Example 1 of coproducts in Section 10.67 of [Adamek] p. 185. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπΆ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β β!β(β:(π΄ β π΅)βΆπΆ β§ (β β (inl βΎ π΄)) = πΉ β§ (β β (inr βΎ π΅)) = πΊ)) | ||
Syntax | ccrd 9933 | Extend class definition to include the cardinal size function. |
class card | ||
Syntax | cale 9934 | Extend class definition to include the aleph function. |
class β΅ | ||
Syntax | ccf 9935 | Extend class definition to include the cofinality function. |
class cf | ||
Syntax | wacn 9936 | The axiom of choice for limited-length sequences. |
class AC π΄ | ||
Definition | df-card 9937* | Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. See cardval 10544 for its value and cardval2 9989 for a simpler version of its value. The principal theorem relating cardinality to equinumerosity is carden 10549. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003.) |
β’ card = (π₯ β V β¦ β© {π¦ β On β£ π¦ β π₯}) | ||
Definition | df-aleph 9938 | Define the aleph function. Our definition expresses Definition 12 of [Suppes] p. 229 in a closed form, from which we derive the recursive definition as Theorems aleph0 10064, alephsuc 10066, and alephlim 10065. The aleph function provides a one-to-one, onto mapping from the ordinal numbers to the infinite cardinal numbers. Roughly, any aleph is the smallest infinite cardinal number whose size is strictly greater than any aleph before it. (Contributed by NM, 21-Oct-2003.) |
β’ β΅ = rec(har, Ο) | ||
Definition | df-cf 9939* | Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 10245 for its value and a description. (Contributed by NM, 1-Apr-2004.) |
β’ cf = (π₯ β On β¦ β© {π¦ β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’))}) | ||
Definition | df-acn 9940* | Define a local and length-limited version of the axiom of choice. The definition of the predicate π β AC π΄ is that for all families of nonempty subsets of π indexed on π΄ (i.e. functions π΄βΆπ« π β {β }), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.) |
β’ AC π΄ = {π₯ β£ (π΄ β V β§ βπ β ((π« π₯ β {β }) βm π΄)βπβπ¦ β π΄ (πβπ¦) β (πβπ¦))} | ||
Theorem | cardf2 9941* | The cardinality function is a function with domain the well-orderable sets. Assuming AC, this is the universe. (Contributed by Mario Carneiro, 6-Jun-2013.) (Revised by Mario Carneiro, 20-Sep-2014.) |
β’ card:{π₯ β£ βπ¦ β On π¦ β π₯}βΆOn | ||
Theorem | cardon 9942 | The cardinal number of a set is an ordinal number. Proposition 10.6(1) of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) (Revised by Mario Carneiro, 13-Sep-2013.) |
β’ (cardβπ΄) β On | ||
Theorem | isnum2 9943* | A way to express well-orderability without bound or distinct variables. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by Mario Carneiro, 27-Apr-2015.) |
β’ (π΄ β dom card β βπ₯ β On π₯ β π΄) | ||
Theorem | isnumi 9944 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β On β§ π΄ β π΅) β π΅ β dom card) | ||
Theorem | ennum 9945 | Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β π΅ β (π΄ β dom card β π΅ β dom card)) | ||
Theorem | finnum 9946 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β Fin β π΄ β dom card) | ||
Theorem | onenon 9947 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β On β π΄ β dom card) | ||
Theorem | tskwe 9948* | A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π β§ {π₯ β π« π΄ β£ π₯ βΊ π΄} β π΄) β π΄ β dom card) | ||
Theorem | xpnum 9949 | The cartesian product of numerable sets is numerable. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β (π΄ Γ π΅) β dom card) | ||
Theorem | cardval3 9950* | An alternate definition of the value of (cardβπ΄) that does not require AC to prove. (Contributed by Mario Carneiro, 7-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.) |
β’ (π΄ β dom card β (cardβπ΄) = β© {π₯ β On β£ π₯ β π΄}) | ||
Theorem | cardid2 9951 | Any numerable set is equinumerous to its cardinal number. Proposition 10.5 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
β’ (π΄ β dom card β (cardβπ΄) β π΄) | ||
Theorem | isnum3 9952 | A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β dom card β (cardβπ΄) β π΄) | ||
Theorem | oncardval 9953* | The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 10544, this theorem does not require the Axiom of Choice. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
β’ (π΄ β On β (cardβπ΄) = β© {π₯ β On β£ π₯ β π΄}) | ||
Theorem | oncardid 9954 | Any ordinal number is equinumerous to its cardinal number. Unlike cardid 10545, this theorem does not require the Axiom of Choice. (Contributed by NM, 26-Jul-2004.) |
β’ (π΄ β On β (cardβπ΄) β π΄) | ||
Theorem | cardonle 9955 | The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85. (Contributed by NM, 22-Oct-2003.) |
β’ (π΄ β On β (cardβπ΄) β π΄) | ||
Theorem | card0 9956 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
β’ (cardββ ) = β | ||
Theorem | cardidm 9957 | The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
β’ (cardβ(cardβπ΄)) = (cardβπ΄) | ||
Theorem | oncard 9958* | A set is a cardinal number iff it equals its own cardinal number. Proposition 10.9 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
β’ (βπ₯ π΄ = (cardβπ₯) β π΄ = (cardβπ΄)) | ||
Theorem | ficardom 9959 | The cardinal number of a finite set is a finite ordinal. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 4-Feb-2013.) |
β’ (π΄ β Fin β (cardβπ΄) β Ο) | ||
Theorem | ficardid 9960 | A finite set is equinumerous to its cardinal number. (Contributed by Mario Carneiro, 21-Sep-2013.) |
β’ (π΄ β Fin β (cardβπ΄) β π΄) | ||
Theorem | cardnn 9961 | The cardinality of a natural number is the number. Corollary 10.23 of [TakeutiZaring] p. 90. (Contributed by Mario Carneiro, 7-Jan-2013.) |
β’ (π΄ β Ο β (cardβπ΄) = π΄) | ||
Theorem | cardnueq0 9962 | The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013.) |
β’ (π΄ β dom card β ((cardβπ΄) = β β π΄ = β )) | ||
Theorem | cardne 9963 | No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 9-Jan-2013.) |
β’ (π΄ β (cardβπ΅) β Β¬ π΄ β π΅) | ||
Theorem | carden2a 9964 | If two sets have equal nonzero cardinalities, then they are equinumerous. This assertion and carden2b 9965 are meant to replace carden 10549 in ZF without AC. (Contributed by Mario Carneiro, 9-Jan-2013.) |
β’ (((cardβπ΄) = (cardβπ΅) β§ (cardβπ΄) β β ) β π΄ β π΅) | ||
Theorem | carden2b 9965 | If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 9964 are meant to replace carden 10549 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) |
β’ (π΄ β π΅ β (cardβπ΄) = (cardβπ΅)) | ||
Theorem | card1 9966* | A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013.) |
β’ ((cardβπ΄) = 1o β βπ₯ π΄ = {π₯}) | ||
Theorem | cardsn 9967 | A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013.) |
β’ (π΄ β π β (cardβ{π΄}) = 1o) | ||
Theorem | carddomi2 9968 | Two sets have the dominance relationship if their cardinalities have the subset relationship and one is numerable. See also carddom 10552, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β π) β ((cardβπ΄) β (cardβπ΅) β π΄ βΌ π΅)) | ||
Theorem | sdomsdomcardi 9969 | A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013.) |
β’ (π΄ βΊ (cardβπ΅) β π΄ βΊ π΅) | ||
Theorem | cardlim 9970 | An infinite cardinal is a limit ordinal. Equivalent to Exercise 4 of [TakeutiZaring] p. 91. (Contributed by Mario Carneiro, 13-Jan-2013.) |
β’ (Ο β (cardβπ΄) β Lim (cardβπ΄)) | ||
Theorem | cardsdomelir 9971 | A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 9972 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.) |
β’ (π΄ β (cardβπ΅) β π΄ βΊ π΅) | ||
Theorem | cardsdomel 9972 | A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 4-Jun-2015.) |
β’ ((π΄ β On β§ π΅ β dom card) β (π΄ βΊ π΅ β π΄ β (cardβπ΅))) | ||
Theorem | iscard 9973* | Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.) |
β’ ((cardβπ΄) = π΄ β (π΄ β On β§ βπ₯ β π΄ π₯ βΊ π΄)) | ||
Theorem | iscard2 9974* | Two ways to express the property of being a cardinal number. Definition 8 of [Suppes] p. 225. (Contributed by Mario Carneiro, 15-Jan-2013.) |
β’ ((cardβπ΄) = π΄ β (π΄ β On β§ βπ₯ β On (π΄ β π₯ β π΄ β π₯))) | ||
Theorem | carddom2 9975 | Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 10552, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β ((cardβπ΄) β (cardβπ΅) β π΄ βΌ π΅)) | ||
Theorem | harcard 9976 | The class of ordinal numbers dominated by a set is a cardinal number. Theorem 59 of [Suppes] p. 228. (Contributed by Mario Carneiro, 20-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ (cardβ(harβπ΄)) = (harβπ΄) | ||
Theorem | cardprclem 9977* | Lemma for cardprc 9978. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ π΄ = {π₯ β£ (cardβπ₯) = π₯} β β’ Β¬ π΄ β V | ||
Theorem | cardprc 9978 | The class of all cardinal numbers is not a set (i.e. is a proper class). Theorem 19.8 of [Eisenberg] p. 310. In this proof (which does not use AC), we cannot use Cantor's construction canth3 10559 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 9542 to construct (effectively) (β΅βsuc π΄) from (β΅βπ΄), which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.) |
β’ {π₯ β£ (cardβπ₯) = π₯} β V | ||
Theorem | carduni 9979* | The union of a set of cardinals is a cardinal. Theorem 18.14 of [Monk1] p. 133. (Contributed by Mario Carneiro, 20-Jan-2013.) |
β’ (π΄ β π β (βπ₯ β π΄ (cardβπ₯) = π₯ β (cardββͺ π΄) = βͺ π΄)) | ||
Theorem | cardiun 9980* | The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.) |
β’ (π΄ β π β (βπ₯ β π΄ (cardβπ΅) = π΅ β (cardββͺ π₯ β π΄ π΅) = βͺ π₯ β π΄ π΅)) | ||
Theorem | cardennn 9981 | If π΄ is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
β’ ((π΄ β π΅ β§ π΅ β Ο) β (cardβπ΄) = π΅) | ||
Theorem | cardsucinf 9982 | The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
β’ ((π΄ β On β§ Ο β π΄) β (cardβsuc π΄) = (cardβπ΄)) | ||
Theorem | cardsucnn 9983 | The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 9982. (Contributed by NM, 7-Nov-2008.) |
β’ (π΄ β Ο β (cardβsuc π΄) = suc (cardβπ΄)) | ||
Theorem | cardom 9984 | The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133. (Contributed by NM, 28-Oct-2003.) |
β’ (cardβΟ) = Ο | ||
Theorem | carden2 9985 | Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 10549, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β ((cardβπ΄) = (cardβπ΅) β π΄ β π΅)) | ||
Theorem | cardsdom2 9986 | A numerable set is strictly dominated by another iff their cardinalities are strictly ordered. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β ((cardβπ΄) β (cardβπ΅) β π΄ βΊ π΅)) | ||
Theorem | domtri2 9987 | Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β (π΄ βΌ π΅ β Β¬ π΅ βΊ π΄)) | ||
Theorem | nnsdomel 9988 | Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅ β π΄ βΊ π΅)) | ||
Theorem | cardval2 9989* | An alternate version of the value of the cardinal number of a set. Compare cardval 10544. This theorem could be used to give a simpler definition of card in place of df-card 9937. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.) |
β’ (π΄ β dom card β (cardβπ΄) = {π₯ β On β£ π₯ βΊ π΄}) | ||
Theorem | isinffi 9990* | An infinite set contains subsets equinumerous to every finite set. Extension of isinf 9263 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
β’ ((Β¬ π΄ β Fin β§ π΅ β Fin) β βπ π:π΅β1-1βπ΄) | ||
Theorem | fidomtri 9991 | Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 27-Apr-2015.) |
β’ ((π΄ β Fin β§ π΅ β π) β (π΄ βΌ π΅ β Β¬ π΅ βΊ π΄)) | ||
Theorem | fidomtri2 9992 | Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 7-May-2015.) |
β’ ((π΄ β π β§ π΅ β Fin) β (π΄ βΌ π΅ β Β¬ π΅ βΊ π΄)) | ||
Theorem | harsdom 9993 | The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β dom card β π΄ βΊ (harβπ΄)) | ||
Theorem | onsdom 9994* | Any well-orderable set is strictly dominated by an ordinal number. (Contributed by Jeff Hankins, 22-Oct-2009.) (Proof shortened by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β dom card β βπ₯ β On π΄ βΊ π₯) | ||
Theorem | harval2 9995* | An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β dom card β (harβπ΄) = β© {π₯ β On β£ π΄ βΊ π₯}) | ||
Theorem | harsucnn 9996 | The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.) |
β’ (π΄ β Ο β (harβπ΄) = suc π΄) | ||
Theorem | cardmin2 9997* | The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013.) |
β’ (βπ₯ β On π΄ βΊ π₯ β (cardββ© {π₯ β On β£ π΄ βΊ π₯}) = β© {π₯ β On β£ π΄ βΊ π₯}) | ||
Theorem | pm54.43lem 9998* | In Theorem *54.43 of [WhiteheadRussell] p. 360, the number 1 is defined as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 9966), so that their π΄ β 1 means, in our notation, π΄ β {π₯ β£ (cardβπ₯) = 1o}. Here we show that this is equivalent to π΄ β 1o so that we can use the latter more convenient notation in pm54.43 9999. (Contributed by NM, 4-Nov-2013.) |
β’ (π΄ β 1o β π΄ β {π₯ β£ (cardβπ₯) = 1o}) | ||
Theorem | pm54.43 9999 |
Theorem *54.43 of [WhiteheadRussell]
p. 360. "From this proposition it
will follow, when arithmetical addition has been defined, that
1+1=2."
See http://en.wikipedia.org/wiki/Principia_Mathematica#Quotations.
This theorem states that two sets of cardinality 1 are disjoint iff
their union has cardinality 2.
Whitehead and Russell define 1 as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 9966), so that their π΄ β 1 means, in our notation, π΄ β {π₯ β£ (cardβπ₯) = 1o} which is the same as π΄ β 1o by pm54.43lem 9998. We do not have several of their earlier lemmas available (which would otherwise be unused by our different approach to arithmetic), so our proof is longer. (It is also longer because we must show every detail.) Theorem dju1p1e2 10171 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.) |
β’ ((π΄ β 1o β§ π΅ β 1o) β ((π΄ β© π΅) = β β (π΄ βͺ π΅) β 2o)) | ||
Theorem | enpr2 10000 | An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 9052. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5364, ax-un 7728. (Revised by BTernaryTau, 30-Dec-2024.) |
β’ ((π΄ β πΆ β§ π΅ β π· β§ π΄ β π΅) β {π΄, π΅} β 2o) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |