Home | Metamath
Proof Explorer Theorem List (p. 76 of 314) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21444) |
Hilbert Space Explorer
(21445-22967) |
Users' Mathboxes
(22968-31305) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rankxpl 7501 | A lower bound on the rank of a cross product. (Contributed by NM, 18-Sep-2006.) |
Theorem | rankxpu 7502 | An upper bound on the rank of a cross product. (Contributed by NM, 18-Sep-2006.) |
Theorem | rankxplim 7503 | The rank of a cross product when the rank of the union of its arguments is a limit ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxpsuc 7506 for the successor case. (Contributed by NM, 19-Sep-2006.) |
Theorem | rankxplim2 7504 | If the rank of a cross product is a limit ordinal, so is the rank of the union of its arguments. (Contributed by NM, 19-Sep-2006.) |
Theorem | rankxplim3 7505 | The rank of a cross product is a limit ordinal iff its union is. (Contributed by NM, 19-Sep-2006.) |
Theorem | rankxpsuc 7506 | The rank of a cross product when the rank of the union of its arguments is a successor ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxplim 7503 for the limit ordinal case. (Contributed by NM, 19-Sep-2006.) |
Theorem | tcwf 7507 | The transitive closure function is well-founded if its argument is. (Contributed by Mario Carneiro, 23-Jun-2013.) |
Theorem | tcrank 7508 | This theorem expresses two different facts from the two subset implications in this equality. In the forward direction, it says that the transitive closure has members of every rank below . Stated another way, to construct a set at a given rank, you have to climb the entire hierarchy of ordinals below , constructing at least one set at each level in order to move up the ranks. In the reverse direction, it says that every member of has a rank below the rank of , since intuitively it contains only the members of and the members of those and so on, but nothing "bigger" than . (Contributed by Mario Carneiro, 23-Jun-2013.) |
Theorem | scottex 7509* | Scott's trick collects all sets that have a certain property and are of smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of [Jech] p. 72, is a set. (Contributed by NM, 13-Oct-2003.) |
Theorem | scott0 7510* | Scott's trick collects all sets that have a certain property and are of smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of [Jech] p. 72, contains at least one representative with the property, if there is one. In other words, the collection is empty iff no set has the property (i.e. is empty). (Contributed by NM, 15-Oct-2003.) |
Theorem | scottexs 7511* | Theorem scheme version of scottex 7509. The collection of all of minimum rank such that is true, is a set. (Contributed by NM, 13-Oct-2003.) |
Theorem | scott0s 7512* | Theorem scheme version of scott0 7510. The collection of all of minimum rank such that is true, is not empty iff there is an such that holds. (Contributed by NM, 13-Oct-2003.) |
Theorem | cplem1 7513* | Lemma for the Collection Principle cp 7515. (Contributed by NM, 17-Oct-2003.) |
Theorem | cplem2 7514* | -Lemma for the Collection Principle cp 7515. (Contributed by NM, 17-Oct-2003.) |
Theorem | cp 7515* | Collection Principle. This remarkable theorem scheme is in effect a very strong generalization of the Axiom of Replacement. The proof makes use of Scott's trick scottex 7509 that collapses a proper class into a set of minimum rank. The wff can be thought of as . Scheme "Collection Principle" of [Jech] p. 72. (Contributed by NM, 17-Oct-2003.) |
Theorem | bnd 7516* | A very strong generalization of the Axiom of Replacement (compare zfrep6 5668), derived from the Collection Principle cp 7515. Its strength lies in the rather profound fact that does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. (Contributed by NM, 17-Oct-2004.) |
Theorem | bnd2 7517* | A variant of the Boundedness Axiom bnd 7516 that picks a subset out of a possibly proper class in which a property is true. (Contributed by NM, 4-Feb-2004.) |
Theorem | kardex 7518* | The collection of all sets equinumerous to a set and having least possible rank is a set. This is the part of the justification of the definition of kard of [Enderton] p. 222. (Contributed by NM, 14-Dec-2003.) |
Theorem | karden 7519* | If we allow the Axiom of Regularity, we can avoid the Axiom of Choice by defining the cardinal number of a set as the set of all sets equinumerous to it and having least possible rank. This theorem proves the equinumerosity relationship for this definition (compare carden 8127). The hypotheses correspond to the definition of kard of [Enderton] p. 222 (which we don't define separately since currently we do not use it elsewhere). This theorem along with kardex 7518 justify the definition of kard. The restriction to least rank prevents the proper class that would result from . (Contributed by NM, 18-Dec-2003.) |
Theorem | htalem 7520* | Lemma for defining an emulation of Hilbert's epsilon. Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/. This theorem is equivalent to Hilbert's "transfinite axiom," described on that page, with the additional antecedent. The element is the epsilon that the theorem emulates. (Contributed by NM, 11-Mar-2004.) (Revised by Mario Carneiro, 25-Jun-2015.) |
Theorem | hta 7521* |
A ZFC emulation of Hilbert's transfinite axiom. The set has the
properties of Hilbert's epsilon, except that it also depends on a
well-ordering .
This theorem arose from discussions with Raph
Levien on 5-Mar-2004 about translating the HOL proof language, which
uses Hilbert's epsilon. See
http://us.metamath.org/downloads/choice.txt
(copy of obsolete link
http://ghilbert.org/choice.txt) and
http://us.metamath.org/downloads/megillaward2005he.pdf.
Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/. This theorem differs from Hilbert's transfinite axiom described on that page in that it requires as an antecedent. Class collects the sets of least rank for which is true. Class , which emulates the epsilon, is the minimum element in a well-ordering on . If a well-ordering on can be expressed in a closed form, as might be the case if we are working with say natural numbers, we can eliminate the antecedent with modus ponens, giving us the exact equivalent of Hilbert's transfinite axiom. Otherwise, we replace with a dummy set variable, say , and attach as an antecedent in each step of the ZFC version of the HOL proof until the epsilon is eliminated. At that point, (which will have as a free variable) will no longer be present, and we can eliminate by applying exlimiv 2024 and weth 8076, using scottexs 7511 to establish the existence of . For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem 7520. (Contributed by NM, 11-Mar-2004.) (Revised by Mario Carneiro, 25-Jun-2015.) |
Syntax | ccrd 7522 | Extend class definition to include the cardinal size function. |
Syntax | cale 7523 | Extend class definition to include the aleph function. |
Syntax | ccf 7524 | Extend class definition to include the cofinality function. |
Syntax | wacn 7525 | The axiom of choice for limited-length sequences. |
AC | ||
Definition | df-card 7526* | 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 8122 for its value, cardval2 7578 for a simpler version of its value. The principle theorem relating cardinality to equinumerosity is carden 8127. 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.) |
Definition | df-aleph 7527 | 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 7647, alephsuc 7649, and alephlim 7648. 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.) |
har | ||
Definition | df-cf 7528* | Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 7827 for its value and a description. (Contributed by NM, 1-Apr-2004.) |
Definition | df-acn 7529* | 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 | ||
Theorem | cardf2 7530* | 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.) |
Theorem | cardon 7531 | 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.) |
Theorem | isnum2 7532* | 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.) |
Theorem | isnumi 7533 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | ennum 7534 | Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | finnum 7535 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | onenon 7536 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | tskwe 7537* | A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | xpnum 7538 | The cartesian product of numerable sets is numerable. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | cardval3 7539* | An alternative definition of the value of that does not require AC to prove. (Contributed by Mario Carneiro, 7-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.) |
Theorem | cardid2 7540 | Any numerable set is equinumerous to its cardinal number. Proposition 10.5 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
Theorem | isnum3 7541 | A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | oncardval 7542* | The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 8122, this theorem does not require the Axiom of Choice. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
Theorem | oncardid 7543 | Any ordinal number is equinumerous to its cardinal number. Unlike cardid 8123, this theorem does not require the Axiom of Choice. (Contributed by NM, 26-Jul-2004.) |
Theorem | cardonle 7544 | 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.) |
Theorem | card0 7545 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
Theorem | cardidm 7546 | The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
Theorem | oncard 7547* | 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.) |
Theorem | ficardom 7548 | 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.) |
Theorem | ficardid 7549 | A finite set is equinumerous to its cardinal number. (Contributed by Mario Carneiro, 21-Sep-2013.) |
Theorem | cardnn 7550 | The cardinality of a natural number is the number. Corollary 10.23 of [TakeutiZaring] p. 90. (Contributed by Mario Carneiro, 7-Jan-2013.) |
Theorem | cardnueq0 7551 | The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013.) |
Theorem | cardne 7552 | 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.) |
Theorem | carden2a 7553 | If two sets have equal nonzero cardinalities, then they are equinumerous. (This assertion and carden2b 7554 are meant to replace carden 8127 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) |
Theorem | carden2b 7554 | If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 7553 are meant to replace carden 8127 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) |
Theorem | card1 7555* | A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013.) |
Theorem | cardsn 7556 | A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013.) |
Theorem | carddomi2 7557 | Two sets have the dominance relationship if their cardinalities have the subset relationship and one is numerable. See also carddom 8130, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | sdomsdomcardi 7558 | A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013.) |
Theorem | cardlim 7559 | An infinite cardinal is a limit ordinal. Equivalent to Exercise 4 of [TakeutiZaring] p. 91. (Contributed by Mario Carneiro, 13-Jan-2013.) |
Theorem | cardsdomelir 7560 | A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 7561 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.) |
Theorem | cardsdomel 7561 | 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.) |
Theorem | iscard 7562* | Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.) |
Theorem | iscard2 7563* | Two ways to express the property of being a cardinal number. Definition 8 of [Suppes] p. 225. (Contributed by Mario Carneiro, 15-Jan-2013.) |
Theorem | carddom2 7564 | Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 8130, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | harcard 7565 | 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.) |
har har | ||
Theorem | cardprclem 7566* | Lemma for cardprc 7567. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
Theorem | cardprc 7567 | 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 8137 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 7213 to construct (effectively) from , which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.) |
Theorem | carduni 7568* | The union of a set of cardinals is a cardinal. Theorem 18.14 of [Monk1] p. 133. (Contributed by Mario Carneiro, 20-Jan-2013.) |
Theorem | cardiun 7569* | The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.) |
Theorem | cardennn 7570 | If is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
Theorem | cardsucinf 7571 | The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
Theorem | cardsucnn 7572 | The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 7571. (Contributed by NM, 7-Nov-2008.) |
Theorem | cardom 7573 | The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133. (Contributed by NM, 28-Oct-2003.) |
Theorem | carden2 7574 | Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 8127, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.) |
Theorem | cardsdom2 7575 | 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.) |
Theorem | domtri2 7576 | Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | nnsdomel 7577 | Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
Theorem | cardval2 7578* | An alternate version of the value of the cardinal number of a set. Compare cardval 8122. This theorem could be used to give us a simpler definition of in place of df-card 7526. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.) |
Theorem | isinffi 7579* | An infinite set contains subsets equinumerous to every finite set. Extension of isinf 7030 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
Theorem | fidomtri 7580 | 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.) |
Theorem | fidomtri2 7581 | 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.) |
Theorem | harsdom 7582 | The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.) |
har | ||
Theorem | onsdom 7583* | 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.) |
Theorem | harval2 7584* | An alternative expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015.) |
har | ||
Theorem | cardmin2 7585* | The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013.) |
Theorem | pm54.43lem 7586* | 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 7555), so that their means, in our notation, . Here we show that this is equivalent to so that we can use the latter more convenient notation in pm54.43 7587. (Contributed by NM, 4-Nov-2013.) |
Theorem | pm54.43 7587 |
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 7555), so that their means, in our notation, which is the same as by pm54.43lem 7586. 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 pm110.643 7757 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.) |
Theorem | pr2nelem 7588 | Lemma for pr2ne 7589. (Contributed by FL, 17-Aug-2008.) |
Theorem | pr2ne 7589 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
Theorem | prdom2 7590 | An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.) |
Theorem | en2eqpr 7591 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
Theorem | dif1card 7592 | The cardinality of a non-empty 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.) |
Theorem | leweon 7593* | Lexicographical order is a well-ordering of . Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 7594, this order is not set-like, as the preimage of is the proper class . (Contributed by Mario Carneiro, 9-Mar-2013.) |
Theorem | r0weon 7594* | 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.) |
Se | ||
Theorem | infxpenlem 7595* | Lemma for infxpen 7596. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
OrdIso | ||
Theorem | infxpen 7596 | Every infinite ordinal is equinumerous to its cross product. 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 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.) |
Theorem | xpomen 7597 | The cross 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 | infxpidm2 7598 | The cross product of an infinite set with itself is idempotent. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of [TakeutiZaring] p. 95. See also infxpidm 8138. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | infxpenc 7599* | A canonical version of infxpen 7596, by a completely different approach (although it uses infxpen 7596 via xpomen 7597). Using Cantor's normal form, we can show that respects equinumerosity (oef1o 7355), so that all the steps of can be verified using bijections to do the ordinal commutations. (The assumption on can be satisfied using cnfcom3c 7363.) (Contributed by Mario Carneiro, 30-May-2015.) |
CNF CNF CNF CNF | ||
Theorem | infxpenc2lem1 7600* | Lemma for infxpenc2 7603. (Contributed by Mario Carneiro, 30-May-2015.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |