Home | Metamath
Proof Explorer Theorem List (p. 71 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | onintrab 7001 | The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003.) |
Theorem | onintrab2 7002 | An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003.) |
Theorem | onnmin 7003 | No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997.) |
Theorem | onnminsb 7004* | An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. is the wff resulting from the substitution of for in wff . (Contributed by NM, 9-Nov-2003.) |
Theorem | oneqmin 7005* | A way to show that an ordinal number equals the minimum of a nonempty collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection. (Contributed by NM, 14-Nov-2003.) |
Theorem | bm2.5ii 7006* | Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.) |
Theorem | onminex 7007* | If a wff is true for an ordinal number, there is the smallest ordinal number for which it is true. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Mario Carneiro, 20-Nov-2016.) |
Theorem | sucon 7008 | The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003.) |
Theorem | sucexb 7009 | A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.) |
Theorem | sucexg 7010 | The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.) |
Theorem | sucex 7011 | The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
Theorem | onmindif2 7012 | The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed. (Contributed by NM, 20-Nov-2003.) |
Theorem | suceloni 7013 | The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.) |
Theorem | ordsuc 7014 | The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995.) |
Theorem | ordpwsuc 7015 | The collection of ordinals in the power class of an ordinal is its successor. (Contributed by NM, 30-Jan-2005.) |
Theorem | onpwsuc 7016 | The collection of ordinal numbers in the power set of an ordinal number is its successor. (Contributed by NM, 19-Oct-2004.) |
Theorem | sucelon 7017 | The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.) |
Theorem | ordsucss 7018 | The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.) |
Theorem | onpsssuc 7019 | An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
Theorem | ordelsuc 7020 | A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 29-Nov-2003.) |
Theorem | onsucmin 7021* | The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.) |
Theorem | ordsucelsuc 7022 | Membership is inherited by successors. Generalization of Exercise 9 of [TakeutiZaring] p. 42. (Contributed by NM, 22-Jun-1998.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Theorem | ordsucsssuc 7023 | The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003.) |
Theorem | ordsucuniel 7024 | Given an element of the union of an ordinal , is an element of itself. (Contributed by Scott Fenton, 28-Mar-2012.) (Proof shortened by Mario Carneiro, 29-May-2015.) |
Theorem | ordsucun 7025 | The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors. (Contributed by NM, 28-Nov-2003.) |
Theorem | ordunpr 7026 | The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015.) |
Theorem | ordunel 7027 | The maximum of two ordinals belongs to a third if each of them do. (Contributed by NM, 18-Sep-2006.) (Revised by Mario Carneiro, 25-Jun-2015.) |
Theorem | onsucuni 7028 | A class of ordinal numbers is a subclass of the successor of its union. Similar to Proposition 7.26 of [TakeutiZaring] p. 41. (Contributed by NM, 19-Sep-2003.) |
Theorem | ordsucuni 7029 | An ordinal class is a subclass of the successor of its union. (Contributed by NM, 12-Sep-2003.) |
Theorem | orduniorsuc 7030 | An ordinal class is either its union or the successor of its union. If we adopt the view that zero is a limit ordinal, this means every ordinal class is either a limit or a successor. (Contributed by NM, 13-Sep-2003.) |
Theorem | unon 7031 | The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40. (Contributed by NM, 12-Nov-2003.) |
Theorem | ordunisuc 7032 | An ordinal class is equal to the union of its successor. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | orduniss2 7033* | The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005.) |
Theorem | onsucuni2 7034 | A successor ordinal is the successor of its union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | 0elsuc 7035 | The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995.) |
Theorem | limon 7036 | The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.) |
Theorem | onssi 7037 | An ordinal number is a subset of . (Contributed by NM, 11-Aug-1994.) |
Theorem | onsuci 7038 | The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.) |
Theorem | onuniorsuci 7039 | An ordinal number is either its own union (if zero or a limit ordinal) or the successor of its union. (Contributed by NM, 13-Jun-1994.) |
Theorem | onuninsuci 7040* | A limit ordinal is not a successor ordinal. (Contributed by NM, 18-Feb-2004.) |
Theorem | onsucssi 7041 | A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 16-Sep-1995.) |
Theorem | nlimsucg 7042 | A successor is not a limit ordinal. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | orduninsuc 7043* | An ordinal equal to its union is not a successor. (Contributed by NM, 18-Feb-2004.) |
Theorem | ordunisuc2 7044* | An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005.) |
Theorem | ordzsl 7045* | An ordinal is zero, a successor ordinal, or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
Theorem | onzsl 7046* | An ordinal number is zero, a successor ordinal, or a limit ordinal number. (Contributed by NM, 1-Oct-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dflim3 7047* | An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor. (Contributed by NM, 1-Nov-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | dflim4 7048* | An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005.) |
Theorem | limsuc 7049 | The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.) |
Theorem | limsssuc 7050 | A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003.) |
Theorem | nlimon 7051* | Two ways to express the class of non-limit ordinal numbers. Part of Definition 7.27 of [TakeutiZaring] p. 42, who use the symbol KI for this class. (Contributed by NM, 1-Nov-2004.) |
Theorem | limuni3 7052* | The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005.) |
Theorem | tfi 7053* |
The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring]
p. 39. This principle states that if is a class of ordinal
numbers with the property that every ordinal number included in
also belongs to , then every ordinal number is in .
See theorem tfindes 7062 or tfinds 7059 for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004.) |
Theorem | tfis 7054* | Transfinite Induction Schema. If all ordinal numbers less than a given number have a property (induction hypothesis), then all ordinal numbers have the property (conclusion). Exercise 25 of [Enderton] p. 200. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 20-Nov-2016.) |
Theorem | tfis2f 7055* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.) |
Theorem | tfis2 7056* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.) |
Theorem | tfis3 7057* | Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003.) |
Theorem | tfisi 7058* | A transfinite induction scheme in "implicit" form where the induction is done on an object derived from the object of interest. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
Theorem | tfinds 7059* | Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 16-Apr-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | tfindsg 7060* | Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal instead of zero. Remark in [TakeutiZaring] p. 57. (Contributed by NM, 5-Mar-2004.) |
Theorem | tfindsg2 7061* | Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal instead of zero. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 5-Jan-2005.) |
Theorem | tfindes 7062* | Transfinite Induction with explicit substitution. The first hypothesis is the basis, the second is the induction step for successors, and the third is the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 5-Mar-2004.) |
Theorem | tfinds2 7063* | Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of [Suppes] p. 197. The wff is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004.) |
Theorem | tfinds3 7064* | Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. (Contributed by NM, 6-Jan-2005.) (Revised by David Abernethy, 21-Jun-2011.) |
Syntax | com 7065 | Extend class notation to include the class of natural numbers. |
Definition | df-om 7066* |
Define the class of natural numbers, which are all ordinal numbers that
are less than every limit ordinal, i.e. all finite ordinals. Our
definition is a variant of the Definition of N of [BellMachover] p. 471.
See dfom2 7067 for an alternate definition. Later, when we
assume the
Axiom of Infinity, we show is a set in omex 8540, and can
then be defined per dfom3 8544 (the smallest inductive set) and dfom4 8546.
Note: the natural numbers are a subset of the ordinal numbers df-on 5727. They are completely different from the natural numbers (df-nn 11021) that are a subset of the complex numbers defined much later in our development, although the two sets have analogous properties and operations defined on them. (Contributed by NM, 15-May-1994.) |
Theorem | dfom2 7067 | An alternate definition of the set of natural numbers . Definition 7.28 of [TakeutiZaring] p. 42, who use the symbol KI for the inner class builder of non-limit ordinal numbers (see nlimon 7051). (Contributed by NM, 1-Nov-2004.) |
Theorem | elom 7068* | Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 8545. (Contributed by NM, 15-May-1994.) |
Theorem | omsson 7069 | Omega is a subset of . (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | limomss 7070 | The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of [TakeutiZaring] p. 44. Remarkably, our proof does not require the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.) |
Theorem | nnon 7071 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
Theorem | nnoni 7072 | A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
Theorem | nnord 7073 | A natural number is ordinal. (Contributed by NM, 17-Oct-1995.) |
Theorem | ordom 7074 | Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | elnn 7075 | A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.) |
Theorem | omon 7076 | The class of natural numbers is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinal numbers (if we deny the Axiom of Infinity). Remark in [TakeutiZaring] p. 43. (Contributed by NM, 10-May-1998.) |
Theorem | omelon2 7077 | Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.) |
Theorem | nnlim 7078 | A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.) |
Theorem | omssnlim 7079 | The class of natural numbers is a subclass of the class of non-limit ordinal numbers. Exercise 4 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | limom 7080 | Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
Theorem | peano2b 7081 | A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.) |
Theorem | nnsuc 7082* | A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.) |
Theorem | ssnlim 7083* | An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) |
Theorem | omsinds 7084* | Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015.) |
Theorem | peano1 7085 | Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 7085 through peano5 7089 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. (Contributed by NM, 15-May-1994.) |
Theorem | peano2 7086 | The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) |
Theorem | peano3 7087 | The successor of any natural number is not zero. One of Peano's five postulates for arithmetic. Proposition 7.30(3) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) |
Theorem | peano4 7088 | Two natural numbers are equal iff their successors are equal, i.e. the successor function is one-to-one. One of Peano's five postulates for arithmetic. Proposition 7.30(4) of [TakeutiZaring] p. 43. (Contributed by NM, 3-Sep-2003.) |
Theorem | peano5 7089* | The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's five postulates for arithmetic. Proposition 7.30(5) of [TakeutiZaring] p. 43, except our proof does not require the Axiom of Infinity. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction step, is derived from this theorem as theorem findes 7096. (Contributed by NM, 18-Feb-2004.) |
Theorem | nn0suc 7090* | A natural number is either 0 or a successor. (Contributed by NM, 27-May-1998.) |
Theorem | find 7091* | The Principle of Finite Induction (mathematical induction). Corollary 7.31 of [TakeutiZaring] p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that is a set of natural numbers, zero belongs to , and given any member of the member's successor also belongs to . The conclusion is that every natural number is in . (Contributed by NM, 22-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Theorem | finds 7092* | Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. This is Metamath 100 proof #74. (Contributed by NM, 14-Apr-1995.) |
Theorem | findsg 7093* | Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. The basis of this version is an arbitrary natural number instead of zero. (Contributed by NM, 16-Sep-1995.) |
Theorem | finds2 7094* | Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 29-Nov-2002.) |
Theorem | finds1 7095* | Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 22-Mar-2006.) |
Theorem | findes 7096 | Finite induction with explicit substitution. The first hypothesis is the basis and the second is the induction step. Theorem Schema 22 of [Suppes] p. 136. See tfindes 7062 for the transfinite version. This is an alternative for Metamath 100 proof #74. (Contributed by Raph Levien, 9-Jul-2003.) |
Theorem | dmexg 7097 | The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.) |
Theorem | rnexg 7098 | The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) |
Theorem | dmex 7099 | The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.) |
Theorem | rnex 7100 | The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |