Home | Metamath
Proof Explorer Theorem List (p. 99 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | updjudhf 9801* | 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 9802* | 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 9803* | 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 9804* | Universal property of the disjoint union. This theorem shows that the disjoint union, together with the left and right injections df-inl 9772 and df-inr 9773, is the coproduct in the category of sets, see Wikipedia "Coproduct", https://en.wikipedia.org/wiki/Coproduct 9773 (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 9805 | Extend class definition to include the cardinal size function. |
class card | ||
Syntax | cale 9806 | Extend class definition to include the aleph function. |
class β΅ | ||
Syntax | ccf 9807 | Extend class definition to include the cofinality function. |
class cf | ||
Syntax | wacn 9808 | The axiom of choice for limited-length sequences. |
class AC π΄ | ||
Definition | df-card 9809* | 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 10416 for its value and cardval2 9861 for a simpler version of its value. The principal theorem relating cardinality to equinumerosity is carden 10421. 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 9810 | 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 9936, alephsuc 9938, and alephlim 9937. 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 9811* | Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 10117 for its value and a description. (Contributed by NM, 1-Apr-2004.) |
β’ cf = (π₯ β On β¦ β© {π¦ β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’))}) | ||
Definition | df-acn 9812* | 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 9813* | 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 9814 | 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 9815* | 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 9816 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β On β§ π΄ β π΅) β π΅ β dom card) | ||
Theorem | ennum 9817 | Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β π΅ β (π΄ β dom card β π΅ β dom card)) | ||
Theorem | finnum 9818 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β Fin β π΄ β dom card) | ||
Theorem | onenon 9819 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β On β π΄ β dom card) | ||
Theorem | tskwe 9820* | A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π β§ {π₯ β π« π΄ β£ π₯ βΊ π΄} β π΄) β π΄ β dom card) | ||
Theorem | xpnum 9821 | 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 9822* | 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 9823 | 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 9824 | A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β dom card β (cardβπ΄) β π΄) | ||
Theorem | oncardval 9825* | The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 10416, 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 9826 | Any ordinal number is equinumerous to its cardinal number. Unlike cardid 10417, this theorem does not require the Axiom of Choice. (Contributed by NM, 26-Jul-2004.) |
β’ (π΄ β On β (cardβπ΄) β π΄) | ||
Theorem | cardonle 9827 | 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 9828 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
β’ (cardββ ) = β | ||
Theorem | cardidm 9829 | The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
β’ (cardβ(cardβπ΄)) = (cardβπ΄) | ||
Theorem | oncard 9830* | 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 9831 | 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 9832 | A finite set is equinumerous to its cardinal number. (Contributed by Mario Carneiro, 21-Sep-2013.) |
β’ (π΄ β Fin β (cardβπ΄) β π΄) | ||
Theorem | cardnn 9833 | 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 9834 | The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013.) |
β’ (π΄ β dom card β ((cardβπ΄) = β β π΄ = β )) | ||
Theorem | cardne 9835 | 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 9836 | If two sets have equal nonzero cardinalities, then they are equinumerous. This assertion and carden2b 9837 are meant to replace carden 10421 in ZF without AC. (Contributed by Mario Carneiro, 9-Jan-2013.) |
β’ (((cardβπ΄) = (cardβπ΅) β§ (cardβπ΄) β β ) β π΄ β π΅) | ||
Theorem | carden2b 9837 | If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 9836 are meant to replace carden 10421 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) |
β’ (π΄ β π΅ β (cardβπ΄) = (cardβπ΅)) | ||
Theorem | card1 9838* | A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013.) |
β’ ((cardβπ΄) = 1o β βπ₯ π΄ = {π₯}) | ||
Theorem | cardsn 9839 | A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013.) |
β’ (π΄ β π β (cardβ{π΄}) = 1o) | ||
Theorem | carddomi2 9840 | Two sets have the dominance relationship if their cardinalities have the subset relationship and one is numerable. See also carddom 10424, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β π) β ((cardβπ΄) β (cardβπ΅) β π΄ βΌ π΅)) | ||
Theorem | sdomsdomcardi 9841 | A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013.) |
β’ (π΄ βΊ (cardβπ΅) β π΄ βΊ π΅) | ||
Theorem | cardlim 9842 | 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 9843 | A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 9844 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.) |
β’ (π΄ β (cardβπ΅) β π΄ βΊ π΅) | ||
Theorem | cardsdomel 9844 | 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 9845* | Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.) |
β’ ((cardβπ΄) = π΄ β (π΄ β On β§ βπ₯ β π΄ π₯ βΊ π΄)) | ||
Theorem | iscard2 9846* | 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 9847 | Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 10424, 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 9848 | 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 9849* | Lemma for cardprc 9850. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ π΄ = {π₯ β£ (cardβπ₯) = π₯} β β’ Β¬ π΄ β V | ||
Theorem | cardprc 9850 | 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 10431 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 9414 to construct (effectively) (β΅βsuc π΄) from (β΅βπ΄), which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.) |
β’ {π₯ β£ (cardβπ₯) = π₯} β V | ||
Theorem | carduni 9851* | 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 9852* | The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.) |
β’ (π΄ β π β (βπ₯ β π΄ (cardβπ΅) = π΅ β (cardββͺ π₯ β π΄ π΅) = βͺ π₯ β π΄ π΅)) | ||
Theorem | cardennn 9853 | If π΄ is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
β’ ((π΄ β π΅ β§ π΅ β Ο) β (cardβπ΄) = π΅) | ||
Theorem | cardsucinf 9854 | The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
β’ ((π΄ β On β§ Ο β π΄) β (cardβsuc π΄) = (cardβπ΄)) | ||
Theorem | cardsucnn 9855 | The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 9854. (Contributed by NM, 7-Nov-2008.) |
β’ (π΄ β Ο β (cardβsuc π΄) = suc (cardβπ΄)) | ||
Theorem | cardom 9856 | 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 9857 | Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 10421, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β ((cardβπ΄) = (cardβπ΅) β π΄ β π΅)) | ||
Theorem | cardsdom2 9858 | 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 9859 | Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β (π΄ βΌ π΅ β Β¬ π΅ βΊ π΄)) | ||
Theorem | nnsdomel 9860 | Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (π΄ β π΅ β π΄ βΊ π΅)) | ||
Theorem | cardval2 9861* | An alternate version of the value of the cardinal number of a set. Compare cardval 10416. This theorem could be used to give a simpler definition of card in place of df-card 9809. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.) |
β’ (π΄ β dom card β (cardβπ΄) = {π₯ β On β£ π₯ βΊ π΄}) | ||
Theorem | isinffi 9862* | An infinite set contains subsets equinumerous to every finite set. Extension of isinf 9138 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
β’ ((Β¬ π΄ β Fin β§ π΅ β Fin) β βπ π:π΅β1-1βπ΄) | ||
Theorem | fidomtri 9863 | 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 9864 | 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 9865 | The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β dom card β π΄ βΊ (harβπ΄)) | ||
Theorem | onsdom 9866* | 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 9867* | 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 9868 | The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.) |
β’ (π΄ β Ο β (harβπ΄) = suc π΄) | ||
Theorem | cardmin2 9869* | 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 9870* | 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 9838), 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 9871. (Contributed by NM, 4-Nov-2013.) |
β’ (π΄ β 1o β π΄ β {π₯ β£ (cardβπ₯) = 1o}) | ||
Theorem | pm54.43 9871 |
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 9838), so that their π΄ β 1 means, in our notation, π΄ β {π₯ β£ (cardβπ₯) = 1o} which is the same as π΄ β 1o by pm54.43lem 9870. 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 10043 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.) |
β’ ((π΄ β 1o β§ π΅ β 1o) β ((π΄ β© π΅) = β β (π΄ βͺ π΅) β 2o)) | ||
Theorem | enpr2 9872 | An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 8927. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5319, ax-un 7663. (Revised by BTernaryTau, 30-Dec-2024.) |
β’ ((π΄ β πΆ β§ π΅ β π· β§ π΄ β π΅) β {π΄, π΅} β 2o) | ||
Theorem | pr2nelemOLD 9873 | Obsolete version of enpr2 9872 as of 30-Dec-2024. (Contributed by FL, 17-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β πΆ β§ π΅ β π· β§ π΄ β π΅) β {π΄, π΅} β 2o) | ||
Theorem | pr2ne 9874 | If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010.) Avoid ax-pow 5319, ax-un 7663. (Revised by BTernaryTau, 30-Dec-2024.) |
β’ ((π΄ β πΆ β§ π΅ β π·) β ({π΄, π΅} β 2o β π΄ β π΅)) | ||
Theorem | pr2neOLD 9875 | Obsolete version of pr2ne 9874 as of 30-Dec-2024. (Contributed by FL, 14-Feb-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β πΆ β§ π΅ β π·) β ({π΄, π΅} β 2o β π΄ β π΅)) | ||
Theorem | prdom2 9876 | An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.) |
β’ ((π΄ β πΆ β§ π΅ β π·) β {π΄, π΅} βΌ 2o) | ||
Theorem | en2eqpr 9877 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
β’ ((πΆ β 2o β§ π΄ β πΆ β§ π΅ β πΆ) β (π΄ β π΅ β πΆ = {π΄, π΅})) | ||
Theorem | en2eleq 9878 | Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ ((π β π β§ π β 2o) β π = {π, βͺ (π β {π})}) | ||
Theorem | en2other2 9879 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ ((π β π β§ π β 2o) β βͺ (π β {βͺ (π β {π})}) = π) | ||
Theorem | dif1card 9880 | The cardinality of a nonempty finite set is one greater than the cardinality of the set with one element removed. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Feb-2013.) |
β’ ((π΄ β Fin β§ π β π΄) β (cardβπ΄) = suc (cardβ(π΄ β {π}))) | ||
Theorem | leweon 9881* | Lexicographical order is a well-ordering of On Γ On. Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 9882, this order is not set-like, as the preimage of β¨1o, β β© is the proper class ({β } Γ On). (Contributed by Mario Carneiro, 9-Mar-2013.) |
β’ πΏ = {β¨π₯, π¦β© β£ ((π₯ β (On Γ On) β§ π¦ β (On Γ On)) β§ ((1st βπ₯) β (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯) β (2nd βπ¦))))} β β’ πΏ We (On Γ On) | ||
Theorem | r0weon 9882* | A set-like well-ordering of the class of ordinal pairs. Proposition 7.58(1) of [TakeutiZaring] p. 54. (Contributed by Mario Carneiro, 7-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
β’ πΏ = {β¨π₯, π¦β© β£ ((π₯ β (On Γ On) β§ π¦ β (On Γ On)) β§ ((1st βπ₯) β (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯) β (2nd βπ¦))))} & β’ π = {β¨π§, π€β© β£ ((π§ β (On Γ On) β§ π€ β (On Γ On)) β§ (((1st βπ§) βͺ (2nd βπ§)) β ((1st βπ€) βͺ (2nd βπ€)) β¨ (((1st βπ§) βͺ (2nd βπ§)) = ((1st βπ€) βͺ (2nd βπ€)) β§ π§πΏπ€)))} β β’ (π We (On Γ On) β§ π Se (On Γ On)) | ||
Theorem | infxpenlem 9883* | Lemma for infxpen 9884. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
β’ πΏ = {β¨π₯, π¦β© β£ ((π₯ β (On Γ On) β§ π¦ β (On Γ On)) β§ ((1st βπ₯) β (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯) β (2nd βπ¦))))} & β’ π = {β¨π§, π€β© β£ ((π§ β (On Γ On) β§ π€ β (On Γ On)) β§ (((1st βπ§) βͺ (2nd βπ§)) β ((1st βπ€) βͺ (2nd βπ€)) β¨ (((1st βπ§) βͺ (2nd βπ§)) = ((1st βπ€) βͺ (2nd βπ€)) β§ π§πΏπ€)))} & β’ π = (π β© ((π Γ π) Γ (π Γ π))) & β’ (π β ((π β On β§ βπ β π (Ο β π β (π Γ π) β π)) β§ (Ο β π β§ βπ β π π βΊ π))) & β’ π = ((1st βπ€) βͺ (2nd βπ€)) & β’ π½ = OrdIso(π, (π Γ π)) β β’ ((π΄ β On β§ Ο β π΄) β (π΄ Γ π΄) β π΄) | ||
Theorem | infxpen 9884 | Every infinite ordinal is equinumerous to its Cartesian square. Proposition 10.39 of [TakeutiZaring] p. 94, whose proof we follow closely. The key idea is to show that the relation π is a well-ordering of (On Γ On) with the additional property that π -initial segments of (π₯ Γ π₯) (where π₯ is a limit ordinal) are of cardinality at most π₯. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
β’ ((π΄ β On β§ Ο β π΄) β (π΄ Γ π΄) β π΄) | ||
Theorem | xpomen 9885 | The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.) |
β’ (Ο Γ Ο) β Ο | ||
Theorem | xpct 9886 | The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
β’ ((π΄ βΌ Ο β§ π΅ βΌ Ο) β (π΄ Γ π΅) βΌ Ο) | ||
Theorem | infxpidm2 9887 | Every infinite well-orderable set is equinumerous to its Cartesian square. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of [TakeutiZaring] p. 95. See also infxpidm 10432. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ Ο βΌ π΄) β (π΄ Γ π΄) β π΄) | ||
Theorem | infxpenc 9888* | A canonical version of infxpen 9884, by a completely different approach (although it uses infxpen 9884 via xpomen 9885). Using Cantor's normal form, we can show that π΄ βo π΅ respects equinumerosity (oef1o 9568), so that all the steps of (Οβπ) Β· (Οβπ) β Οβ(2π) β (Οβ2)βπ β Οβπ can be verified using bijections to do the ordinal commutations. (The assumption on π can be satisfied using cnfcom3c 9576.) (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
β’ (π β π΄ β On) & β’ (π β Ο β π΄) & β’ (π β π β (On β 1o)) & β’ (π β πΉ:(Ο βo 2o)β1-1-ontoβΟ) & β’ (π β (πΉββ ) = β ) & β’ (π β π:π΄β1-1-ontoβ(Ο βo π)) & β’ πΎ = (π¦ β {π₯ β ((Ο βo 2o) βm π) β£ π₯ finSupp β } β¦ (πΉ β (π¦ β β‘( I βΎ π)))) & β’ π» = (((Ο CNF π) β πΎ) β β‘((Ο βo 2o) CNF π)) & β’ πΏ = (π¦ β {π₯ β (Ο βm (π Β·o 2o)) β£ π₯ finSupp β } β¦ (( I βΎ Ο) β (π¦ β β‘(π β β‘π)))) & β’ π = (π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€)) & β’ π = (π§ β 2o, π€ β π β¦ ((2o Β·o π€) +o π§)) & β’ π½ = (((Ο CNF (2o Β·o π)) β πΏ) β β‘(Ο CNF (π Β·o 2o))) & β’ π = (π₯ β (Ο βo π), π¦ β (Ο βo π) β¦ (((Ο βo π) Β·o π₯) +o π¦)) & β’ π = (π₯ β π΄, π¦ β π΄ β¦ β¨(πβπ₯), (πβπ¦)β©) & β’ πΊ = (β‘π β (((π» β π½) β π) β π)) β β’ (π β πΊ:(π΄ Γ π΄)β1-1-ontoβπ΄) | ||
Theorem | infxpenc2lem1 9889* | Lemma for infxpenc2 9892. (Contributed by Mario Carneiro, 30-May-2015.) |
β’ (π β π΄ β On) & β’ (π β βπ β π΄ (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) & β’ π = (β‘(π₯ β (On β 1o) β¦ (Ο βo π₯))βran (πβπ)) β β’ ((π β§ (π β π΄ β§ Ο β π)) β (π β (On β 1o) β§ (πβπ):πβ1-1-ontoβ(Ο βo π))) | ||
Theorem | infxpenc2lem2 9890* | Lemma for infxpenc2 9892. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
β’ (π β π΄ β On) & β’ (π β βπ β π΄ (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) & β’ π = (β‘(π₯ β (On β 1o) β¦ (Ο βo π₯))βran (πβπ)) & β’ (π β πΉ:(Ο βo 2o)β1-1-ontoβΟ) & β’ (π β (πΉββ ) = β ) & β’ πΎ = (π¦ β {π₯ β ((Ο βo 2o) βm π) β£ π₯ finSupp β } β¦ (πΉ β (π¦ β β‘( I βΎ π)))) & β’ π» = (((Ο CNF π) β πΎ) β β‘((Ο βo 2o) CNF π)) & β’ πΏ = (π¦ β {π₯ β (Ο βm (π Β·o 2o)) β£ π₯ finSupp β } β¦ (( I βΎ Ο) β (π¦ β β‘(π β β‘π)))) & β’ π = (π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€)) & β’ π = (π§ β 2o, π€ β π β¦ ((2o Β·o π€) +o π§)) & β’ π½ = (((Ο CNF (2o Β·o π)) β πΏ) β β‘(Ο CNF (π Β·o 2o))) & β’ π = (π₯ β (Ο βo π), π¦ β (Ο βo π) β¦ (((Ο βo π) Β·o π₯) +o π¦)) & β’ π = (π₯ β π, π¦ β π β¦ β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©) & β’ πΊ = (β‘(πβπ) β (((π» β π½) β π) β π)) β β’ (π β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) | ||
Theorem | infxpenc2lem3 9891* | Lemma for infxpenc2 9892. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
β’ (π β π΄ β On) & β’ (π β βπ β π΄ (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) & β’ π = (β‘(π₯ β (On β 1o) β¦ (Ο βo π₯))βran (πβπ)) & β’ (π β πΉ:(Ο βo 2o)β1-1-ontoβΟ) & β’ (π β (πΉββ ) = β ) β β’ (π β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) | ||
Theorem | infxpenc2 9892* | Existence form of infxpenc 9888. A "uniform" or "canonical" version of infxpen 9884, asserting the existence of a single function π that simultaneously demonstrates product idempotence of all ordinals below a given bound. (Contributed by Mario Carneiro, 30-May-2015.) |
β’ (π΄ β On β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) | ||
Theorem | iunmapdisj 9893* | The union βͺ π β πΆ(π΄ βm π) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.) |
β’ β*π β πΆ π΅ β (π΄ βm π) | ||
Theorem | fseqenlem1 9894* | Lemma for fseqen 9897. (Contributed by Mario Carneiro, 17-May-2015.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π΄) & β’ (π β πΉ:(π΄ Γ π΄)β1-1-ontoβπ΄) & β’ πΊ = seqΟ((π β V, π β V β¦ (π₯ β (π΄ βm suc π) β¦ ((πβ(π₯ βΎ π))πΉ(π₯βπ)))), {β¨β , π΅β©}) β β’ ((π β§ πΆ β Ο) β (πΊβπΆ):(π΄ βm πΆ)β1-1βπ΄) | ||
Theorem | fseqenlem2 9895* | Lemma for fseqen 9897. (Contributed by Mario Carneiro, 17-May-2015.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π΄) & β’ (π β πΉ:(π΄ Γ π΄)β1-1-ontoβπ΄) & β’ πΊ = seqΟ((π β V, π β V β¦ (π₯ β (π΄ βm suc π) β¦ ((πβ(π₯ βΎ π))πΉ(π₯βπ)))), {β¨β , π΅β©}) & β’ πΎ = (π¦ β βͺ π β Ο (π΄ βm π) β¦ β¨dom π¦, ((πΊβdom π¦)βπ¦)β©) β β’ (π β πΎ:βͺ π β Ο (π΄ βm π)β1-1β(Ο Γ π΄)) | ||
Theorem | fseqdom 9896* | One half of fseqen 9897. (Contributed by Mario Carneiro, 18-Nov-2014.) |
β’ (π΄ β π β (Ο Γ π΄) βΌ βͺ π β Ο (π΄ βm π)) | ||
Theorem | fseqen 9897* | A set that is equinumerous to its Cartesian product is equinumerous to the set of finite sequences on it. (This can be proven more easily using some choice but this proof avoids it.) (Contributed by Mario Carneiro, 18-Nov-2014.) |
β’ (((π΄ Γ π΄) β π΄ β§ π΄ β β ) β βͺ π β Ο (π΄ βm π) β (Ο Γ π΄)) | ||
Theorem | infpwfidom 9898 | The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption (π« π΄ β© Fin) β V because this theorem also implies that π΄ is a set if π« π΄ β© Fin is.) (Contributed by Mario Carneiro, 17-May-2015.) |
β’ ((π« π΄ β© Fin) β V β π΄ βΌ (π« π΄ β© Fin)) | ||
Theorem | dfac8alem 9899* | Lemma for dfac8a 9900. If the power set of a set has a choice function, then the set is numerable. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 5-Jan-2013.) |
β’ πΉ = recs(πΊ) & β’ πΊ = (π β V β¦ (πβ(π΄ β ran π))) β β’ (π΄ β πΆ β (βπβπ¦ β π« π΄(π¦ β β β (πβπ¦) β π¦) β π΄ β dom card)) | ||
Theorem | dfac8a 9900* | Numeration theorem: every set with a choice function on its power set is numerable. With AC, this reduces to the statement that every set is numerable. Similar to Theorem 10.3 of [TakeutiZaring] p. 84. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 5-Jan-2013.) |
β’ (π΄ β π΅ β (βββπ¦ β π« π΄(π¦ β β β (ββπ¦) β π¦) β π΄ β dom card)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |