Home | Metamath
Proof Explorer Theorem List (p. 78 of 324) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-22370) |
Hilbert Space Explorer
(22371-23893) |
Users' Mathboxes
(23894-32378) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rankr1c 7701 | A relationship between the rank function and the cumulative hierarchy of sets function . Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankidn 7702 | A relationship between the rank function and the cumulative hierarchy of sets function . (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankpwi 7703 | The rank of a power set. Part of Exercise 30 of [Enderton] p. 207. (Contributed by Mario Carneiro, 3-Jun-2013.) |
Theorem | rankelb 7704 | The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | wfelirr 7705 | A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 7520. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | rankval3b 7706* | The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | ranksnb 7707 | The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112. (Contributed by Mario Carneiro, 10-Jun-2013.) |
Theorem | rankonidlem 7708 | Lemma for rankonid 7709. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.) |
Theorem | rankonid 7709 | The rank of an ordinal number is itself. Proposition 9.18 of [TakeutiZaring] p. 79 and its converse. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | onwf 7710 | The ordinals are all well-founded. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | onssr1 7711 | Initial segments of the ordinals are contained in initial segments of the cumulative hierarchy. (Contributed by FL, 20-Apr-2011.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankr1g 7712 | A relationship between the rank function and the cumulative hierarchy of sets function . Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankid 7713 | Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankr1 7714 | A relationship between the rank function and the cumulative hierarchy of sets function . Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by NM, 6-Oct-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2014.) |
Theorem | ssrankr1 7715 | A relationship between an ordinal number less than or equal to a rank, and the cumulative hierarchy of sets . Proposition 9.15(3) of [TakeutiZaring] p. 79. (Contributed by NM, 8-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankr1a 7716 | A relationship between rank and , clearly equivalent to ssrankr1 7715 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 7744 for the subset verion. (Contributed by Raph Levien, 29-May-2004.) |
Theorem | r1val2 7717* | The value of the cumulative hierarchy of sets function expressed in terms of rank. Definition 15.19 of [Monk1] p. 113. (Contributed by NM, 30-Nov-2003.) |
Theorem | r1val3 7718* | The value of the cumulative hierarchy of sets function expressed in terms of rank. Theorem 15.18 of [Monk1] p. 113. (Contributed by NM, 30-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankel 7719 | The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankval3 7720* | The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | bndrank 7721* | Any class whose elements have bounded rank is a set. Proposition 9.19 of [TakeutiZaring] p. 80. (Contributed by NM, 13-Oct-2003.) |
Theorem | unbndrank 7722* | The elements of a proper class have unbounded rank. Exercise 2 of [TakeutiZaring] p. 80. (Contributed by NM, 13-Oct-2003.) |
Theorem | rankpw 7723 | The rank of a power set. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 22-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | ranklim 7724 | The rank of a set belongs to a limit ordinal iff the rank of its power set does. (Contributed by NM, 18-Sep-2006.) |
Theorem | r1pw 7725 | A stronger property of than rankpw 7723. The latter merely proves that of the successor is a power set, but here we prove that if is in the cumulative hierarchy, then is in the cumulative hierarchy of the successor. (Contributed by Raph Levien, 29-May-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | r1pwOLD 7726 | A stronger property of than rankpw 7723. The latter merely proves that of the successor is a power set, but here we prove that if is in the cumulative hierarchy, then is in the cumulative hierarchy of the successor. (Contributed by Raph Levien, 29-May-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | r1pwcl 7727 | The cumulative hierarchy of a limit ordinal is closed under power set. (Contributed by Raph Levien, 29-May-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankssb 7728 | The subset relation is inherited by the rank function. Exercise 1 of [TakeutiZaring] p. 80. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankss 7729 | The subset relation is inherited by the rank function. Exercise 1 of [TakeutiZaring] p. 80. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankunb 7730 | The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankprb 7731 | The rank of an unordered pair. Part of Exercise 30 of [Enderton] p. 207. (Contributed by Mario Carneiro, 10-Jun-2013.) |
Theorem | rankopb 7732 | The rank of an ordered pair. Part of Exercise 4 of [Kunen] p. 107. (Contributed by Mario Carneiro, 10-Jun-2013.) |
Theorem | rankuni2b 7733* | The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 8-Jun-2013.) |
Theorem | ranksn 7734 | The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112. (Contributed by NM, 28-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankuni2 7735* | The rank of a union. Part of Theorem 15.17(iv) of [Monk1] p. 112. (Contributed by NM, 30-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankun 7736 | The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112. (Contributed by NM, 26-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankpr 7737 | The rank of an unordered pair. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 28-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankop 7738 | The rank of an ordered pair. Part of Exercise 4 of [Kunen] p. 107. (Contributed by NM, 13-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | r1rankid 7739 | Any set is a subset of the hierarchy of its rank. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankeq0b 7740 | A set is empty iff its rank is empty. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankeq0 7741 | A set is empty iff its rank is empty. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankr1id 7742 | The rank of the hierarchy of an ordinal number is itself. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankuni 7743 | The rank of a union. Part of Exercise 4 of [Kunen] p. 107. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankr1b 7744 | A relationship between rank and . See rankr1a 7716 for the membership version. (Contributed by NM, 15-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | ranksuc 7745 | The rank of a successor. (Contributed by NM, 18-Sep-2006.) |
Theorem | rankuniss 7746 | Upper bound of the rank of a union. Part of Exercise 30 of [Enderton] p. 207. (Contributed by NM, 30-Nov-2003.) |
Theorem | rankval4 7747* | The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of [Jech] p. 72. Also a special case of Theorem 7V(b) of [Enderton] p. 204. (Contributed by NM, 12-Oct-2003.) |
Theorem | rankbnd 7748* | The rank of a set is bounded by a bound for the successor of its members. (Contributed by NM, 18-Sep-2006.) |
Theorem | rankbnd2 7749* | The rank of a set is bounded by the successor of a bound for its members. (Contributed by NM, 15-Sep-2006.) |
Theorem | rankc1 7750* | A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.) |
Theorem | rankc2 7751* | A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006.) |
Theorem | rankelun 7752 | Rank membership is inherited by union. (Contributed by NM, 18-Sep-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankelpr 7753 | Rank membership is inherited by unordered pairs. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | rankelop 7754 | Rank membership is inherited by ordered pairs. (Contributed by NM, 18-Sep-2006.) |
Theorem | rankxpl 7755 | A lower bound on the rank of a cross product. (Contributed by NM, 18-Sep-2006.) |
Theorem | rankxpu 7756 | An upper bound on the rank of a cross product. (Contributed by NM, 18-Sep-2006.) |
Theorem | rankxplim 7757 | 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 7760 for the successor case. (Contributed by NM, 19-Sep-2006.) |
Theorem | rankxplim2 7758 | 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 7759 | The rank of a cross product is a limit ordinal iff its union is. (Contributed by NM, 19-Sep-2006.) |
Theorem | rankxpsuc 7760 | 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 7757 for the limit ordinal case. (Contributed by NM, 19-Sep-2006.) |
Theorem | tcwf 7761 | The transitive closure function is well-founded if its argument is. (Contributed by Mario Carneiro, 23-Jun-2013.) |
Theorem | tcrank 7762 | 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 7763* | Scott's trick collects all sets that have a certain property and are of the 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 7764* | Scott's trick collects all sets that have a certain property and are of the 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 7765* | Theorem scheme version of scottex 7763. The collection of all of minimum rank such that is true, is a set. (Contributed by NM, 13-Oct-2003.) |
Theorem | scott0s 7766* | Theorem scheme version of scott0 7764. 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 7767* | Lemma for the Collection Principle cp 7769. (Contributed by NM, 17-Oct-2003.) |
Theorem | cplem2 7768* | -Lemma for the Collection Principle cp 7769. (Contributed by NM, 17-Oct-2003.) |
Theorem | cp 7769* | 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 7763 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 7770* | A very strong generalization of the Axiom of Replacement (compare zfrep6 5925), derived from the Collection Principle cp 7769. 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 7771* | A variant of the Boundedness Axiom bnd 7770 that picks a subset out of a possibly proper class in which a property is true. (Contributed by NM, 4-Feb-2004.) |
Theorem | kardex 7772* | The collection of all sets equinumerous to a set and having the 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 7773* | 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 the least possible rank. This theorem proves the equinumerosity relationship for this definition (compare carden 8380). 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 7772 justify the definition of kard. The restriction to the least rank prevents the proper class that would result from . (Contributed by NM, 18-Dec-2003.) |
Theorem | htalem 7774* | 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 7775* |
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 the 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 1641 and weth 8329, using scottexs 7765 to establish the existence of . For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem 7774. (Contributed by NM, 11-Mar-2004.) (Revised by Mario Carneiro, 25-Jun-2015.) |
Syntax | ccrd 7776 | Extend class definition to include the cardinal size function. |
Syntax | cale 7777 | Extend class definition to include the aleph function. |
Syntax | ccf 7778 | Extend class definition to include the cofinality function. |
Syntax | wacn 7779 | The axiom of choice for limited-length sequences. |
AC | ||
Definition | df-card 7780* | 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 8375 for its value, cardval2 7832 for a simpler version of its value. The principle theorem relating cardinality to equinumerosity is carden 8380. 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 7781 | 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 7901, alephsuc 7903, and alephlim 7902. 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 7782* | Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 8081 for its value and a description. (Contributed by NM, 1-Apr-2004.) |
Definition | df-acn 7783* | 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 7784* | 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 7785 | 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 7786* | 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 7787 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | ennum 7788 | Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | finnum 7789 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | onenon 7790 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | tskwe 7791* | A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | xpnum 7792 | The cartesian product of numerable sets is numerable. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | cardval3 7793* | 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 7794 | 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 7795 | A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | oncardval 7796* | The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 8375, this theorem does not require the Axiom of Choice. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
Theorem | oncardid 7797 | Any ordinal number is equinumerous to its cardinal number. Unlike cardid 8376, this theorem does not require the Axiom of Choice. (Contributed by NM, 26-Jul-2004.) |
Theorem | cardonle 7798 | 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 7799 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
Theorem | cardidm 7800 | The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |